Theory More_Refinement_Libs.WB_More_Refinement_Loops
theory WB_More_Refinement_Loops
imports
Weidenbach_Book_Base.WB_List_More
"HOL-Library.Cardinality"
"HOL-Eisbach.Eisbach"
"HOL-Library.Rewrite"
"Refine_Monadic.Refine_While"
"Refine_Monadic.Refine_Foreach"
begin
lemma SPEC_add_information: ‹P ⟹ A ≤ SPEC Q ⟹ A ≤ SPEC(λx. Q x ∧ P)›
by auto
lemma bind_refine_spec: ‹(⋀x. Φ x ⟹ f x ≤ ⇓ R M) ⟹ M' ≤ SPEC Φ ⟹ M' ⤜ f ≤ ⇓ R M›
by (auto simp add: pw_le_iff refine_pw_simps)
lemma intro_spec_iff:
‹(RES X ⤜ f ≤ M) = (∀x∈X. f x ≤ M)›
using intro_spec_refine_iff[of X f Id M] by auto
lemma case_prod_bind:
assumes ‹⋀x1 x2. x = (x1, x2) ⟹ f x1 x2 ≤ ⇓ R I›
shows ‹(case x of (x1, x2) ⇒ f x1 x2) ≤ ⇓ R I›
using assms by (cases x) auto
lemma (in transfer) transfer_bool[refine_transfer]:
assumes "α fa ≤ Fa"
assumes "α fb ≤ Fb"
shows "α (case_bool fa fb x) ≤ case_bool Fa Fb x"
using assms by (auto split: bool.split)
lemma ref_two_step': ‹A ≤ B ⟹ ⇓ R A ≤ ⇓ R B›
by (auto intro: ref_two_step)
lemma RES_RETURN_RES: ‹RES Φ ⤜ (λT. RETURN (f T)) = RES (f ` Φ)›
by (simp add: bind_RES_RETURN_eq setcompr_eq_image)
lemma RES_RES_RETURN_RES: ‹RES A ⤜ (λT. RES (f T)) = RES (⋃(f ` A))›
by (auto simp: pw_eq_iff refine_pw_simps)
lemma RES_RES2_RETURN_RES: ‹RES A ⤜ (λ(T, T'). RES (f T T')) = RES (⋃(uncurry f ` A))›
by (auto simp: pw_eq_iff refine_pw_simps uncurry_def)
lemma RES_RES3_RETURN_RES:
‹RES A ⤜ (λ(T, T', T''). RES (f T T' T'')) = RES (⋃((λ(a, b, c). f a b c) ` A))›
by (auto simp: pw_eq_iff refine_pw_simps uncurry_def)
lemma meta_same_imp_rule: "(⟦PROP P; PROP P⟧ ⟹ PROP Q) ≡ (PROP P ⟹ PROP Q)"
by rule
lemma split_prod_bound: "(λp. f p) = (λ(a,b). f (a,b))" by auto
lemma RES_RETURN_RES3:
‹SPEC Φ ⤜ (λ(T, T', T''). RETURN (f T T' T'')) = RES ((λ(a, b, c). f a b c) ` {T. Φ T})›
using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c). f a b c›]
apply (subst (asm)(2) split_prod_bound)
apply (subst (asm)(3) split_prod_bound)
by auto
lemma RES_RES_RETURN_RES2: ‹RES A ⤜ (λ(T, T'). RETURN (f T T')) = RES (uncurry f ` A)›
by (auto simp: pw_eq_iff refine_pw_simps uncurry_def)
lemma bind_refine_res: ‹(⋀x. x ∈ Φ ⟹ f x ≤ ⇓ R M) ⟹ M' ≤ RES Φ ⟹ M' ⤜ f ≤ ⇓ R M›
by (auto simp add: pw_le_iff refine_pw_simps)
lemma RES_RETURN_RES_RES2:
‹RES Φ ⤜ (λ(T, T'). RETURN (f T T')) = RES (uncurry f ` Φ)›
using RES_RES2_RETURN_RES[of ‹Φ› ‹λT T'. {f T T'}›]
apply (subst (asm)(2) split_prod_bound)
by (auto simp: RETURN_def uncurry_def)
text ‹
This theorem adds the invariant at the beginning of next iteration to the current invariant,
i.e., the invariant is added as a post-condition on the current iteration.
This is useful to reduce duplication in theorems while refining.
›
lemma RECT_WHILEI_body_add_post_condition:
‹REC⇩T (WHILEI_body (⤜) RETURN I' b' f) x' =
(REC⇩T (WHILEI_body (⤜) RETURN (λx'. I' x' ∧ (b' x' ⟶ f x' = FAIL ∨ f x' ≤ SPEC I')) b' f) x')›
(is ‹REC⇩T ?f x' = REC⇩T ?f' x'›)
proof -
have le: ‹flatf_gfp ?f x' ≤ flatf_gfp ?f' x'› for x'
proof (induct arbitrary: x' rule: flatf_ord.fixp_induct[where b = top and
f = ?f'])
case 1
then show ?case
unfolding fun_lub_def pw_le_iff
by (rule ccpo.admissibleI)
(smt chain_fun flat_lub_in_chain mem_Collect_eq nofail_simps(1))
next
case 2
then show ?case by (auto simp: WHILEI_mono_ge)
next
case 3
then show ?case by simp
next
case (4 x)
have ‹(RES X ⤜ f ≤ M) = (∀x∈X. f x ≤ M)› for x f M X
using intro_spec_refine_iff[of _ _ ‹Id›] by auto
thm bind_refine_RES(2)[of _ Id, simplified]
have [simp]: ‹flatf_mono FAIL (WHILEI_body (⤜) RETURN I' b' f)›
by (simp add: WHILEI_mono_ge)
have ‹flatf_gfp ?f x' = ?f (?f (flatf_gfp ?f)) x'›
apply (subst flatf_ord.fixp_unfold)
apply (solves ‹simp›)
apply (subst flatf_ord.fixp_unfold)
apply (solves ‹simp›)
..
also have ‹… = WHILEI_body (⤜)
RETURN (λx'. I' x' ∧ (b' x' ⟶ f x' = FAIL ∨ f x' ≤ SPEC I')) b' f
(WHILEI_body (⤜) RETURN I' b' f (flatf_gfp (WHILEI_body (⤜) RETURN I' b' f))) x'›
apply (subst (1) WHILEI_body_def, subst (1) WHILEI_body_def)
apply (subst (2) WHILEI_body_def, subst (2) WHILEI_body_def)
apply simp_all
apply (cases ‹f x'›)
apply (auto simp: RES_RETURN_RES nofail_def[symmetric] pw_RES_bind_choose
split: if_splits)
done
also have ‹… = WHILEI_body (⤜)
RETURN (λx'. I' x' ∧ (b' x' ⟶ f x' = FAIL ∨ f x' ≤ SPEC I')) b' f
((flatf_gfp (WHILEI_body (⤜) RETURN I' b' f))) x'›
apply (subst (2) flatf_ord.fixp_unfold)
apply (solves ‹simp›)
..
finally have unfold1: ‹flatf_gfp (WHILEI_body (⤜) RETURN I' b' f) x' =
?f' (flatf_gfp (WHILEI_body (⤜) RETURN I' b' f)) x'›
.
have [intro!]: ‹(⋀x. g x ≤ (h:: 'a ⇒ 'a nres) x) ⟹ fx ⤜ g ≤ fx ⤜ h› for g h fx fy
by (refine_rcg bind_refine'[where R = ‹Id›, simplified]) fast
show ?case
apply (subst unfold1)
using 4 unfolding WHILEI_body_def by auto
qed
have ge: ‹flatf_gfp ?f x' ≥ flatf_gfp ?f' x'› for x'
proof (induct arbitrary: x' rule: flatf_ord.fixp_induct[where b = top and
f = ?f])
case 1
then show ?case
unfolding fun_lub_def pw_le_iff
by (rule ccpo.admissibleI) (smt chain_fun flat_lub_in_chain mem_Collect_eq nofail_simps(1))
next
case 2
then show ?case by (auto simp: WHILEI_mono_ge)
next
case 3
then show ?case by simp
next
case (4 x)
have ‹(RES X ⤜ f ≤ M) = (∀x∈X. f x ≤ M)› for x f M X
using intro_spec_refine_iff[of _ _ ‹Id›] by auto
thm bind_refine_RES(2)[of _ Id, simplified]
have [simp]: ‹flatf_mono FAIL ?f'›
by (simp add: WHILEI_mono_ge)
have H: ‹A = FAIL ⟷ ¬nofail A› for A by (auto simp: nofail_def)
have ‹flatf_gfp ?f' x' = ?f' (?f' (flatf_gfp ?f')) x'›
apply (subst flatf_ord.fixp_unfold)
apply (solves ‹simp›)
apply (subst flatf_ord.fixp_unfold)
apply (solves ‹simp›)
..
also have ‹… = ?f (?f' (flatf_gfp ?f')) x'›
apply (subst (1) WHILEI_body_def, subst (1) WHILEI_body_def)
apply (subst (2) WHILEI_body_def, subst (2) WHILEI_body_def)
apply simp_all
apply (cases ‹f x'›)
apply (auto simp: RES_RETURN_RES nofail_def[symmetric] pw_RES_bind_choose
eq_commute[of ‹FAIL›] H
split: if_splits
cong: if_cong)
done
also have ‹… = ?f (flatf_gfp ?f') x'›
apply (subst (2) flatf_ord.fixp_unfold)
apply (solves ‹simp›)
..
finally have unfold1: ‹flatf_gfp ?f' x' =
?f (flatf_gfp ?f') x'›
.
have [intro!]: ‹(⋀x. g x ≤(h:: 'a ⇒ 'a nres) x) ⟹ fx ⤜ g ≤ fx ⤜ h› for g h fx fy
by (refine_rcg bind_refine'[where R = ‹Id›, simplified]) fast
show ?case
apply (subst unfold1)
using 4
unfolding WHILEI_body_def
by (auto intro: bind_refine'[where R = ‹Id›, simplified])
qed
show ?thesis
unfolding RECT_def
using le[of x'] ge[of x'] by (auto simp: WHILEI_body_trimono)
qed
lemma WHILEIT_add_post_condition:
‹(WHILEIT I' b' f' x') =
(WHILEIT (λx'. I' x' ∧ (b' x' ⟶ f' x' = FAIL ∨ f' x' ≤ SPEC I'))
b' f' x')›
unfolding WHILEIT_def
apply (subst RECT_WHILEI_body_add_post_condition)
..
lemma WHILEIT_rule_stronger_inv:
assumes
‹wf R› and
‹I s› and
‹I' s› and
‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I s' ∧ I' s' ∧ (s', s) ∈ R)› and
‹⋀s. I s ⟹ I' s ⟹ ¬ b s ⟹ Φ s›
shows ‹WHILE⇩T⇗I⇖ b f s ≤ SPEC Φ›
proof -
have ‹WHILE⇩T⇗I⇖ b f s ≤ WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s›
by (metis (mono_tags, lifting) WHILEIT_weaken)
also have ‹WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s ≤ SPEC Φ›
by (rule WHILEIT_rule) (use assms in ‹auto simp: ›)
finally show ?thesis .
qed
lemma RES_RETURN_RES2:
‹SPEC Φ ⤜ (λ(T, T'). RETURN (f T T')) = RES (uncurry f ` {T. Φ T})›
using RES_RETURN_RES[of ‹Collect Φ› ‹uncurry f›]
apply (subst (asm)(2) split_prod_bound)
by auto
lemma WHILEIT_rule_stronger_inv_RES:
assumes
‹wf R› and
‹I s› and
‹I' s›
‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I s' ∧ I' s' ∧ (s', s) ∈ R)› and
‹⋀s. I s ⟹ I' s ⟹ ¬ b s ⟹ s ∈ Φ›
shows ‹WHILE⇩T⇗I⇖ b f s ≤ RES Φ›
proof -
have RES_SPEC: ‹RES Φ = SPEC(λs. s ∈ Φ)›
by auto
have ‹WHILE⇩T⇗I⇖ b f s ≤ WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s›
by (metis (mono_tags, lifting) WHILEIT_weaken)
also have ‹WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s ≤ RES Φ›
unfolding RES_SPEC
by (rule WHILEIT_rule) (use assms in ‹auto simp: ›)
finally show ?thesis .
qed
subsubsection ‹Merge Post-Conditions›
lemma Down_add_assumption_middle:
assumes
‹nofail U› and
‹V ≤ ⇓ {(T1, T0). Q T1 T0 ∧ P T1 ∧ Q' T1 T0} U› and
‹W ≤ ⇓ {(T2, T1). R T2 T1} V›
shows ‹W ≤ ⇓ {(T2, T1). R T2 T1 ∧ P T1} V›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by blast
lemma Down_del_assumption_middle:
assumes
‹S1 ≤ ⇓ {(T1, T0). Q T1 T0 ∧ P T1 ∧ Q' T1 T0} S0›
shows ‹S1 ≤ ⇓ {(T1, T0). Q T1 T0 ∧ Q' T1 T0} S0›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by blast
lemma Down_add_assumption_beginning:
assumes
‹nofail U› and
‹V ≤ ⇓ {(T1, T0). P T1 ∧ Q' T1 T0} U› and
‹W ≤ ⇓ {(T2, T1). R T2 T1} V›
shows ‹W ≤ ⇓ {(T2, T1). R T2 T1 ∧ P T1} V›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by blast
lemma Down_add_assumption_beginning_single:
assumes
‹nofail U› and
‹V ≤ ⇓ {(T1, T0). P T1} U› and
‹W ≤ ⇓ {(T2, T1). R T2 T1} V›
shows ‹W ≤ ⇓ {(T2, T1). R T2 T1 ∧ P T1} V›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by blast
lemma Down_del_assumption_beginning:
fixes U :: ‹'a nres› and V :: ‹'b nres› and Q Q' :: ‹'b ⇒ 'a ⇒ bool›
assumes
‹V ≤ ⇓ {(T1, T0). Q T1 T0 ∧ Q' T1 T0} U›
shows ‹V ≤ ⇓ {(T1, T0). Q' T1 T0} U›
using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by blast
method unify_Down_invs2_normalisation_post =
((unfold meta_same_imp_rule True_implies_equals conj_assoc)?)
method unify_Down_invs2 =
(match premises in
I: ‹S1 ≤ ⇓ R10 S0› and
J[thin]: ‹S2 ≤ ⇓ R21 S1›
for S1:: ‹'b nres› and S0 :: ‹'a nres› and S2 :: ‹'c nres› and R10 R21 ⇒
‹insert True_implies_equals[where P = ‹S2 ≤ ⇓ R21 S1›, symmetric,
THEN equal_elim_rule1, OF J]›
¦ I[thin]: ‹S1 ≤ ⇓ {(T1, T0). P T1} S0› (multi) and
J[thin]: _ for S1:: ‹'b nres› and S0 :: ‹'a nres› and P :: ‹'b ⇒ bool› ⇒
‹match J[uncurry] in
J[curry]: ‹_ ⟹ S2 ≤ ⇓ {(T2, T1). R T2 T1} S1› for S2 :: ‹'c nres› and R ⇒
‹insert Down_add_assumption_beginning_single[where P = P and R = R and
W = S2 and V = S1 and U = S0, OF _ I J];
unify_Down_invs2_normalisation_post›
¦ _ ⇒ ‹fail››
¦ I[thin]: ‹S1 ≤ ⇓ {(T1, T0). P T1 ∧ Q' T1 T0} S0› (multi) and
J[thin]: _ for S1:: ‹'b nres› and S0 :: ‹'a nres› and Q' and P :: ‹'b ⇒ bool› ⇒
‹match J[uncurry] in
J[curry]: ‹_ ⟹ S2 ≤ ⇓ {(T2, T1). R T2 T1} S1› for S2 :: ‹'c nres› and R ⇒
‹insert Down_add_assumption_beginning[where Q' = Q' and P = P and R = R and
W = S2 and V = S1 and U = S0,
OF _ I J];
insert Down_del_assumption_beginning[where Q = ‹λS _. P S› and Q' = Q' and V = S1 and
U = S0, OF I];
unify_Down_invs2_normalisation_post›
¦ _ ⇒ ‹fail››
¦ I[thin]: ‹S1 ≤ ⇓ {(T1, T0). Q T0 T1∧ Q' T1 T0} S0› (multi) and
J: _ for S1:: ‹'b nres› and S0 :: ‹'a nres› and Q Q' ⇒
‹match J[uncurry] in
J[curry]: ‹_ ⟹ S2 ≤ ⇓ {(T2, T1). R T2 T1} S1› for S2 :: ‹'c nres› and R ⇒
‹insert Down_del_assumption_beginning[where Q = ‹λ x y. Q y x› and Q' = Q', OF I];
unify_Down_invs2_normalisation_post›
¦ _ ⇒ ‹fail››
)
text ‹Example:›
lemma
assumes
‹nofail S0› and
1: ‹S1 ≤ ⇓ {(T1, T0). Q T1 T0 ∧ P T1 ∧ P' T1 ∧ P''' T1 ∧ Q' T1 T0 ∧ P42 T1} S0› and
2: ‹S2 ≤ ⇓ {(T2, T1). R T2 T1} S1›
shows ‹S2
≤ ⇓ {(T2, T1).
R T2 T1 ∧
P T1 ∧ P' T1 ∧ P''' T1 ∧ P42 T1}
S1›
using assms apply -
apply unify_Down_invs2+
apply fast
done
subsubsection ‹Inversion Tactics›
lemma refinement_trans_long:
‹A = A' ⟹ B = B' ⟹ R ⊆ R' ⟹ A ≤ ⇓ R B ⟹ A' ≤ ⇓ R' B'›
by (meson pw_ref_iff subsetCE)
lemma mem_set_trans:
‹A ⊆ B ⟹ a ∈ A ⟹ a ∈ B›
by auto
lemma fun_rel_syn_invert:
‹a = a' ⟹ b ⊆ b' ⟹ (fun_rel_syn a b) ⊆ (a' → b')›
by (auto simp: refine_rel_defs)
lemma nres_rel_mono:
‹a ⊆ a' ⟹ ⟨a⟩ nres_rel ⊆ ⟨a'⟩ nres_rel›
by (fastforce simp: refine_rel_defs nres_rel_def pw_ref_iff)
lemma weaken_SPEC2: ‹m' ≤ SPEC Φ ⟹ m = m' ⟹ (⋀x. Φ x ⟹ Ψ x) ⟹ m ≤ SPEC Ψ›
using weaken_SPEC by auto
method match_spec_trans =
(match conclusion in ‹f ≤ SPEC R› for f :: ‹'a nres› and R :: ‹'a ⇒ bool› ⇒
‹print_term f; match premises in I: ‹_ ⟹ _ ⟹ f' ≤ SPEC R'› for f' :: ‹'a nres› and
R' :: ‹'a ⇒ bool›
⇒ ‹print_term f'; rule weaken_SPEC2[of f' R' f R]››)
lemma bind_rule_complete_RES: ‹(M ⤜ f ≤ RES Φ) = (M ≤ SPEC (λx. f x ≤ RES Φ))›
by (auto simp: pw_le_iff refine_pw_simps)
subsubsection ‹More Simplification Theorems›
lemma nofail_Down_nofail: ‹nofail gS ⟹ fS ≤ ⇓ R gS ⟹ nofail fS›
using pw_ref_iff by blast
text ‹This is the refinement version of @{thm WHILEIT_add_post_condition}.›
lemma WHILEIT_refine_with_post:
assumes R0: "I' x' ⟹ (x,x')∈R"
assumes IREF: "⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ I x"
assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R; I x; I' x' ⟧ ⟹ b x = b' x'"
assumes STEP_REF:
"⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x'; f' x' ≤ SPEC I' ⟧ ⟹ f x ≤ ⇓R (f' x')"
shows "WHILEIT I b f x ≤⇓R (WHILEIT I' b' f' x')"
apply (subst (2) WHILEIT_add_post_condition)
apply (rule WHILEIT_refine)
subgoal using R0 by blast
subgoal using IREF by blast
subgoal using COND_REF by blast
subgoal using STEP_REF by auto
done
subsection ‹Some Refinement›
lemma Collect_eq_comp: ‹{(c, a). a = f c} O {(x, y). P x y} = {(c, y). P (f c) y}›
by auto
lemma Collect_eq_comp_right:
‹{(x, y). P x y} O {(c, a). a = f c} = {(x, c). ∃y. P x y ∧ c = f y} ›
by auto
lemma no_fail_spec_le_RETURN_itself: ‹nofail f ⟹ f ≤ SPEC(λx. RETURN x ≤ f)›
by (metis RES_rule nres_order_simps(21) the_RES_inv)
lemma refine_add_invariants':
assumes
‹f S ≤ ⇓ {(S, S'). Q' S S' ∧ Q S} gS› and
‹y ≤ ⇓ {((i, S), S'). P i S S'} (f S)› and
‹nofail gS›
shows ‹y ≤ ⇓ {((i, S), S'). P i S S' ∧ Q S'} (f S)›
using assms unfolding pw_le_iff pw_conc_inres pw_conc_nofail
by force
lemma "weaken_⇓": ‹R' ⊆ R ⟹ f ≤ ⇓ R' g ⟹ f ≤ ⇓ R g›
by (meson pw_ref_iff subset_eq)
method match_Down =
(match conclusion in ‹f ≤ ⇓ R g› for f g R ⇒
‹match premises in I: ‹f ≤ ⇓ R' g› for R'
⇒ ‹rule "weaken_⇓"[OF _ I]››)
lemma Ball2_split_def: ‹(∀(x, y) ∈ A. P x y) ⟷ (∀x y. (x, y) ∈ A ⟶ P x y)›
by blast
lemma in_pair_collect_simp: "(a,b)∈{(a,b). P a b} ⟷ P a b"
by auto
lemma refine_SPEC_refine_Down:
‹f ≤ SPEC C ⟷ f ≤ ⇓ {(T', T). T = T' ∧ C T'} (SPEC C)›
apply (rule iffI)
subgoal
by (rule SPEC_refine) auto
subgoal
by (metis (no_types, lifting) RETURN_ref_SPECD SPEC_cons_rule dual_order.trans
in_pair_collect_simp no_fail_spec_le_RETURN_itself nofail_Down_nofail nofail_simps(2))
done
lemma Down_id_eq: "⇓ Id a = a"
by auto
lemma Down_itself_via_SPEC:
assumes ‹I ≤ SPEC P› and ‹⋀x. P x ⟹ (x, x) ∈ R›
shows ‹I ≤ ⇓ R I›
using assms by (meson inres_SPEC pw_ref_I)
lemma RES_ASSERT_moveout:
"(⋀a. a ∈ P ⟹ Q a) ⟹ do {a ← RES P; ASSERT(Q a); (f a)} =
do {a← RES P; (f a)}"
apply (subst dual_order.eq_iff)
apply (rule conjI)
subgoal
by (refine_rcg bind_refine_RES[where R=Id, unfolded Down_id_eq])
auto
subgoal
by (refine_rcg bind_refine_RES[where R=Id, unfolded Down_id_eq])
auto
done
lemma bind_if_inverse:
‹do {
S ← H;
if b then f S else g S
} =
(if b then do {S ← H; f S} else do {S ← H; g S})
› for H :: ‹'a nres›
by auto
lemma bind_cong_nres: ‹(⋀x. g x = g' x) ⟹ (do {a ← f :: 'a nres; g a}) =
(do {a ← f :: 'a nres; g' a})›
by auto
lemma case_prod_cong:
‹(⋀a b. f a b = g a b) ⟹ (case x of (a, b) ⇒ f a b) = (case x of (a, b) ⇒ g a b)›
by (cases x) auto
lemma if_replace_cond: ‹(if b then P b else Q b) = (if b then P True else Q False)›
by auto
lemma foldli_cong2:
assumes
le: ‹length l = length l'› and
σ: ‹σ = σ'› and
c: ‹c = c'› and
H: ‹⋀σ x. x < length l ⟹ c' σ ⟹ f (l ! x) σ = f' (l' ! x) σ›
shows ‹foldli l c f σ = foldli l' c' f' σ'›
proof -
show ?thesis
using le H unfolding c[symmetric] σ[symmetric]
proof (induction l arbitrary: l' σ)
case Nil
then show ?case by simp
next
case (Cons a l l'') note IH=this(1) and le = this(2) and H = this(3)
show ?case
using le H[of ‹Suc _›] H[of 0] IH[of ‹tl l''› ‹f' (hd l'') σ›]
by (cases l'') auto
qed
qed
lemma foldli_foldli_list_nth:
‹foldli xs c P a = foldli [0..<length xs] c (λi. P (xs ! i)) a›
proof (induction xs arbitrary: a)
case Nil
then show ?case by auto
next
case (Cons x xs) note IH = this(1)
have 1: ‹[0..<length (x # xs)] = 0 # [1..<length (x#xs)]›
by (subst upt_rec) simp
have 2: ‹[1..<length (x#xs)] = map Suc [0..<length xs]›
by (induction xs) auto
have AB: ‹foldli [0..<length (x # xs)] c (λi. P ((x # xs) ! i)) a =
foldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a›
(is ‹?A = ?B›)
unfolding 1 ..
{
assume [simp]: ‹c a›
have ‹foldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a =
foldli [1..<length (x#xs)] c (λi. P ((x # xs) ! i)) (P x a)›
by simp
also have ‹… = foldli [0..<length xs] c (λi. P (xs ! i)) (P x a)›
unfolding 2
by (rule foldli_cong2) auto
finally have ‹?A = foldli [0..<length xs] c (λi. P (xs ! i)) (P x a)›
using AB
by simp
}
moreover {
assume [simp]: ‹¬c a›
have ‹?B = a›
by simp
}
ultimately show ?case by (auto simp: IH)
qed
lemma RES_RES13_RETURN_RES: ‹do {
(M, N, D, Q, W, vm, φ, clvls, cach, lbd, outl, stats, fast_ema, slow_ema, ccount,
vdom, avdom, lcount) ← RES A;
RES (f M N D Q W vm φ clvls cach lbd outl stats fast_ema slow_ema ccount
vdom avdom lcount)
} = RES (⋃(M, N, D, Q, W, vm, φ, clvls, cach, lbd, outl, stats, fast_ema, slow_ema, ccount,
vdom, avdom, lcount)∈A. f M N D Q W vm φ clvls cach lbd outl stats fast_ema slow_ema ccount
vdom avdom lcount)›
by (force simp: pw_eq_iff refine_pw_simps uncurry_def)
lemma RES_SPEC_conv: ‹RES P = SPEC (λv. v ∈ P)›
by auto
lemma add_invar_refineI_P: ‹A ≤ ⇓ {(x,y). R x y} B ⟹ (nofail A ⟹A ≤ SPEC P) ⟹
A ≤ ⇓ {(x,y). R x y ∧ P x} B›
using add_invar_refineI[of ‹λ_. A› _ _ ‹λ_. B› P, where R=‹{(x,y). R x y}› and I=P]
by auto
lemma (in -)WHILEIT_rule_stronger_inv_RES':
assumes
‹wf R› and
‹I s› and
‹I' s›
‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I s' ∧ I' s' ∧ (s', s) ∈ R)› and
‹⋀s. I s ⟹ I' s ⟹ ¬ b s ⟹ RETURN s ≤ ⇓ H (RES Φ)›
shows ‹WHILE⇩T⇗I⇖ b f s ≤ ⇓ H (RES Φ)›
proof -
have RES_SPEC: ‹RES Φ = SPEC(λs. s ∈ Φ)›
by auto
have ‹WHILE⇩T⇗I⇖ b f s ≤ WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s›
by (metis (mono_tags, lifting) WHILEIT_weaken)
also have ‹WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s ≤ ⇓ H (RES Φ)›
unfolding RES_SPEC conc_fun_SPEC
apply (rule WHILEIT_rule[OF assms(1)])
subgoal using assms(2,3) by auto
subgoal using assms(4) by auto
subgoal using assms(5) unfolding RES_SPEC conc_fun_SPEC by auto
done
finally show ?thesis .
qed
lemma same_in_Id_option_rel:
‹x = x' ⟹ (x, x') ∈ ⟨Id⟩option_rel›
by auto
definition find_in_list_between :: ‹('a ⇒ bool) ⇒ nat ⇒ nat ⇒ 'a list ⇒ nat option nres› where
‹find_in_list_between P a b C = do {
(x, _) ← WHILE⇩T⇗λ(found, i). i ≥ a ∧ i ≤ length C ∧ i ≤ b ∧ (∀j∈{a..<i}. ¬P (C!j)) ∧
(∀j. found = Some j ⟶ (i = j ∧ P (C ! j) ∧ j < b ∧ j ≥ a))⇖
(λ(found, i). found = None ∧ i < b)
(λ(_, i). do {
ASSERT(i < length C);
if P (C!i) then RETURN (Some i, i) else RETURN (None, i+1)
})
(None, a);
RETURN x
}›
lemma find_in_list_between_spec:
assumes ‹a ≤ length C› and ‹b ≤ length C› and ‹a ≤ b›
shows
‹find_in_list_between P a b C ≤ SPEC(λi.
(i ≠ None ⟶ P (C ! the i) ∧ the i ≥ a ∧ the i < b) ∧
(i = None ⟶ (∀j. j ≥ a ⟶ j < b ⟶ ¬P (C!j))))›
unfolding find_in_list_between_def
apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(f, i). Suc (length C) -
(i + (if f = None then 0 else 1)))›])
subgoal by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms 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
subgoal by auto
subgoal by auto
subgoal by (auto simp: less_Suc_eq)
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
done
lemma nfoldli_cong2:
assumes
le: ‹length l = length l'› and
σ: ‹σ = σ'› and
c: ‹c = c'› and
H: ‹⋀σ x. x < length l ⟹ c' σ ⟹ f (l ! x) σ = f' (l' ! x) σ›
shows ‹nfoldli l c f σ = nfoldli l' c' f' σ'›
proof -
show ?thesis
using le H unfolding c[symmetric] σ[symmetric]
proof (induction l arbitrary: l' σ)
case Nil
then show ?case by simp
next
case (Cons a l l'') note IH=this(1) and le = this(2) and H = this(3)
show ?case
using le H[of ‹Suc _›] H[of 0] IH[of ‹tl l''› ‹_›]
by (cases l'')
(auto intro: bind_cong_nres)
qed
qed
lemma nfoldli_nfoldli_list_nth:
‹nfoldli xs c P a = nfoldli [0..<length xs] c (λi. P (xs ! i)) a›
proof (induction xs arbitrary: a)
case Nil
then show ?case by auto
next
case (Cons x xs) note IH = this(1)
have 1: ‹[0..<length (x # xs)] = 0 # [1..<length (x#xs)]›
by (subst upt_rec) simp
have 2: ‹[1..<length (x#xs)] = map Suc [0..<length xs]›
by (induction xs) auto
have AB: ‹nfoldli [0..<length (x # xs)] c (λi. P ((x # xs) ! i)) a =
nfoldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a›
(is ‹?A = ?B›)
unfolding 1 ..
{
assume [simp]: ‹c a›
have ‹nfoldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a =
do {
σ ← (P x a);
nfoldli [1..<length (x#xs)] c (λi. P ((x # xs) ! i)) σ
}›
by simp
moreover have ‹nfoldli [1..<length (x#xs)] c (λi. P ((x # xs) ! i)) σ =
nfoldli [0..<length xs] c (λi. P (xs ! i)) σ› for σ
unfolding 2
by (rule nfoldli_cong2) auto
ultimately have ‹?A = do {
σ ← (P x a);
nfoldli [0..<length xs] c (λi. P (xs ! i)) σ
}›
using AB
by (auto intro: bind_cong_nres)
}
moreover {
assume [simp]: ‹¬c a›
have ‹?B = RETURN a›
by simp
}
ultimately show ?case by (auto simp: IH intro: bind_cong_nres)
qed
definition "list_mset_rel ≡ br mset (λ_. True)"
lemma
Nil_list_mset_rel_iff:
‹([], aaa) ∈ list_mset_rel ⟷ aaa = {#}› and
empty_list_mset_rel_iff:
‹(a, {#}) ∈ list_mset_rel ⟷ a = []›
by (auto simp: list_mset_rel_def br_def)
definition list_rel_mset_rel where list_rel_mset_rel_internal:
‹list_rel_mset_rel ≡ λR. ⟨R⟩list_rel O list_mset_rel›
lemma list_rel_mset_rel_def[refine_rel_defs]:
‹⟨R⟩list_rel_mset_rel = ⟨R⟩list_rel O list_mset_rel›
unfolding relAPP_def list_rel_mset_rel_internal ..
lemma list_rel_mset_rel_imp_same_length: ‹(a, b) ∈ ⟨R⟩list_rel_mset_rel ⟹ length a = size b›
by (auto simp: list_rel_mset_rel_def list_mset_rel_def br_def
dest: list_rel_imp_same_length)
lemma while_upt_while_direct1:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} ≤ do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b); σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
apply (refine_vcg WHILET_refine[where R = ‹{((l, x'), (i::nat, x::'a)). x= x' ∧ i ≤ b ∧ i ≥ a ∧
l = drop (i-a) [a..<b]}›])
subgoal by auto
subgoal by (auto simp: FOREACH_cond_def)
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by auto
done
lemma while_upt_while_direct2:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} ≥ do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b); σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
apply (refine_vcg WHILET_refine[where R = ‹{((i::nat, x::'a), (l, x')). x= x' ∧ i ≤ b ∧ i ≥ a ∧
l = drop (i-a) [a..<b]}›])
subgoal by auto
subgoal by (auto simp: FOREACH_cond_def)
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by auto
done
lemma while_upt_while_direct:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} = do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b); σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
using while_upt_while_direct1[of a b] while_upt_while_direct2[of a b]
unfolding dual_order.eq_iff by fast
lemma while_nfoldli:
"do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
RETURN σ
} ≤ nfoldli l c f σ"
apply (induct l arbitrary: σ)
apply (subst WHILET_unfold)
apply (simp add: FOREACH_cond_def)
apply (subst WHILET_unfold)
apply (auto
simp: FOREACH_cond_def FOREACH_body_def
intro: bind_mono Refine_Basic.bind_mono(1))
done
lemma nfoldli_while: "nfoldli l c f σ
≤
(WHILE⇩T⇗I⇖
(FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l, σ) ⤜
(λ(_, σ). RETURN σ))"
proof (induct l arbitrary: σ)
case Nil thus ?case by (subst WHILEIT_unfold) (auto simp: FOREACH_cond_def)
next
case (Cons x ls)
show ?case
proof (cases "c σ")
case False thus ?thesis
apply (subst WHILEIT_unfold)
unfolding FOREACH_cond_def
by simp
next
case [simp]: True
from Cons show ?thesis
apply (subst WHILEIT_unfold)
unfolding FOREACH_cond_def FOREACH_body_def
apply clarsimp
apply (rule Refine_Basic.bind_mono)
apply simp_all
done
qed
qed
lemma while_eq_nfoldli: "do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
RETURN σ
} = nfoldli l c f σ"
apply (rule antisym)
apply (rule while_nfoldli)
apply (rule order_trans[OF nfoldli_while[where I="λ_. True"]])
apply (simp add: WHILET_def)
done
lemma RES_RETURN_RES5:
‹SPEC Φ ⤜ (λ(T1, T2, T3, T4, T5). RETURN (f T1 T2 T3 T4 T5)) =
RES ((λ(a, b, c, d, e). f a b c d e) ` {T. Φ T})›
using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c, d, e). f a b c d e›]
apply (subst (asm)(2) split_prod_bound)
apply (subst (asm)(3) split_prod_bound)
apply (subst (asm)(4) split_prod_bound)
apply (subst (asm)(5) split_prod_bound)
by simp
lemma RES_RETURN_RES6:
‹SPEC Φ ⤜ (λ(T1, T2, T3, T4, T5, T6). RETURN (f T1 T2 T3 T4 T5 T6)) =
RES ((λ(a, b, c, d, e, f'). f a b c d e f') ` {T. Φ T})›
using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c, d, e, f'). f a b c d e f'›]
apply (subst (asm)(2) split_prod_bound)
apply (subst (asm)(3) split_prod_bound)
apply (subst (asm)(4) split_prod_bound)
apply (subst (asm)(5) split_prod_bound)
apply (subst (asm)(6) split_prod_bound)
by simp
lemma RES_RETURN_RES7:
‹SPEC Φ ⤜ (λ(T1, T2, T3, T4, T5, T6, T7). RETURN (f T1 T2 T3 T4 T5 T6 T7)) =
RES ((λ(a, b, c, d, e, f', g). f a b c d e f' g) ` {T. Φ T})›
using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c, d, e, f', g). f a b c d e f' g›]
apply (subst (asm)(2) split_prod_bound)
apply (subst (asm)(3) split_prod_bound)
apply (subst (asm)(4) split_prod_bound)
apply (subst (asm)(5) split_prod_bound)
apply (subst (asm)(6) split_prod_bound)
apply (subst (asm)(7) split_prod_bound)
by simp
lemma RES_RES7_RETURN_RES:
‹RES A ⤜ (λ(a, b, c, d, e, g, h). RES (f a b c d e g h)) =
RES (⋃((λ(a, b, c, d, e, g, h). f a b c d e g h) ` A))›
by (auto simp: pw_eq_iff refine_pw_simps uncurry_def Bex_def
split: prod.splits)
lemma RES_RES8_RETURN_RES:
‹RES A ⤜ (λ(a, b, c, d, e, g, h, i). RES (f a b c d e g h i)) =
RES (⋃((λ(a, b, c, d, e, g, h, i). f a b c d e g h i) ` A))›
by (auto simp: pw_eq_iff refine_pw_simps uncurry_def Bex_def
split: prod.splits)
lemma RES_RES9_RETURN_RES:
‹RES A ⤜ (λ(a, b, c, d, e, g, h, i, j). RES (f a b c d e g h i j)) =
RES (⋃((λ(a, b, c, d, e, g, h, i, j). f a b c d e g h i j) ` A))›
by (auto simp: pw_eq_iff refine_pw_simps uncurry_def Bex_def
split: prod.splits)
lemma fold_eq_nfoldli:
"RETURN (fold f l s) = nfoldli l (λ_. True) (λx s. RETURN (f x s)) s"
by (induction l arbitrary: s) auto
text ‹this is the less dumb version of the refinement for while loops, keeping the loop invariant.›
lemma WHILEIT_refine_with_all_loopinvariants:
assumes R0: "I' x' ⟹ (x,x')∈R"
assumes IREF: "⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ I x"
assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R; I x; I' x' ⟧ ⟹ b x = b' x'"
assumes STEP_REF:
"⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x'; f' x' ≤ SPEC I' ⟧ ⟹ f x ≤ ⇓R (f' x')"
shows "WHILEIT I b f x ≤⇓{(a,b). (a,b) ∈ R ∧ I a ∧ I' b} (WHILEIT I' b' f' x')"
apply (subst (2) WHILEIT_add_post_condition)
apply (rule WHILEIT_refine)
subgoal using R0 IREF by blast
subgoal using IREF by blast
subgoal using COND_REF by blast
subgoal using STEP_REF apply auto
by (smt (verit, best) IREF in_pair_collect_simp inres_SPEC pw_ref_iff)
done
text ‹This lemma cannot be moved to \<^theory>‹Weidenbach_Book_Base.WB_List_More›, because the syntax
\<^term>‹CARD('a)› does not exist there.›
lemma finite_length_le_CARD:
assumes ‹distinct (xs :: 'a :: finite list)›
shows ‹length xs ≤ CARD('a)›
proof -
have ‹set xs ⊆ UNIV›
by auto
show ?thesis
by (metis assms card_ge_UNIV distinct_card le_cases)
qed
lemma WHILEIT_refine_with_invariant_and_break:
assumes R0: ‹I' x' ⟹ (x,x')∈R›
assumes IREF: ‹⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ I x›
assumes COND_REF: ‹⋀x x'. ⟦ (x,x')∈R; I x; I' x' ⟧ ⟹ b x = b' x'›
assumes STEP_REF:
‹⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x' ⟧ ⟹ f x ≤ ⇓R (f' x')›
shows ‹WHILEIT I b f x ≤⇓{(x, x'). (x, x') ∈ R ∧ I x ∧ I' x' ∧ ¬b' x'} (WHILEIT I' b' f' x')›
(is ‹_ ≤ ⇓?R' _›)
apply (subst (2)WHILEIT_add_post_condition)
apply (refine_vcg WHILEIT_refine_genR[where R'=R and R = ?R'])
subgoal by (auto intro: assms)[]
subgoal by (auto intro: assms)[]
subgoal using COND_REF by (auto)
subgoal by (auto intro: assms)[]
subgoal by (auto intro: assms)[]
done
end