theory WB_More_Refinement
imports Weidenbach_Book_Base.WB_List_More
"HOL-Library.Cardinality"
"HOL-Library.Rewrite"
"HOL-Eisbach.Eisbach"
Refine_Monadic.Refine_Basic
Automatic_Refinement.Automatic_Refinement
Automatic_Refinement.Relators
Refine_Monadic.Refine_While
Refine_Monadic.Refine_Foreach
begin
hide_const Autoref_Fix_Rel.CONSTRAINT
definition fref :: "('c ⇒ bool) ⇒ ('a × 'c) set ⇒ ('b × 'd) set
⇒ (('a ⇒ 'b) × ('c ⇒ 'd)) set"
("[_]⇩f _ → _" [0,60,60] 60)
where "[P]⇩f R → S ≡ {(f,g). ∀x y. P y ∧ (x,y)∈R ⟶ (f x, g y)∈S}"
abbreviation freft ("_ →⇩f _" [60,60] 60) where "R →⇩f S ≡ ([λ_. True]⇩f R → S)"
lemma frefI[intro?]:
assumes "⋀x y. ⟦P y; (x,y)∈R⟧ ⟹ (f x, g y)∈S"
shows "(f,g)∈fref P R S"
using assms
unfolding fref_def
by auto
lemma fref_mono: "⟦ ⋀x. P' x ⟹ P x; R' ⊆ R; S ⊆ S' ⟧
⟹ fref P R S ⊆ fref P' R' S'"
unfolding fref_def
by auto blast
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
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
subsection ‹Some Tooling for Refinement›
text ‹
The following very simple tactics remove duplicate variables generated by some tactic like
‹refine_rcg›. For example, if the problem contains \<^term>‹(i, C) = (xa, xb)›, then only
\<^term>‹i› and \<^term>‹C› will remain. It can also prove trivial goals where the goals already
appears in the assumptions.
›
method remove_dummy_vars uses simps =
((unfold prod.inject)?; (simp only: prod.inject)?; (elim conjE)?;
hypsubst?; (simp only: triv_forall_equality simps)?)
subsubsection ‹From @{text →} to @{text ⇓}›
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
ML ‹
signature MORE_REFINEMENT = sig
val down_converse: Proof.context -> thm -> thm
end
structure More_Refinement: MORE_REFINEMENT = struct
val unfold_refine = (fn context => Local_Defs.unfold (context)
@{thms refine_rel_defs nres_rel_def in_pair_collect_simp})
val unfold_Ball = (fn context => Local_Defs.unfold (context)
@{thms Ball2_split_def all_to_meta})
val replace_ALL_by_meta = (fn context => fn thm => Object_Logic.rulify context thm)
val down_converse = (fn context =>
replace_ALL_by_meta context o (unfold_Ball context) o (unfold_refine context))
end
›
attribute_setup "to_⇓" = ‹
Scan.succeed (Thm.rule_attribute [] (More_Refinement.down_converse o Context.proof_of))
› "convert theorem from @{text →}-form to @{text ⇓}-form."
method "to_⇓" =
(unfold refine_rel_defs nres_rel_def in_pair_collect_simp;
unfold Ball2_split_def all_to_meta;
intro allI impI)
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' ⟹ a → b ⊆ a' → b'›
by (auto simp: refine_rel_defs)
lemma fref_param1: "R→S = fref (λ_. True) R S"
by (auto simp: fref_def fun_relD)
lemma fref_syn_invert:
‹a = a' ⟹ b ⊆ b' ⟹ a →⇩f b ⊆ a' →⇩f b'›
unfolding fref_param1[symmetric]
by (rule fun_rel_syn_invert)
lemma nres_rel_mono:
‹a ⊆ a' ⟹ ⟨a⟩ nres_rel ⊆ ⟨a'⟩ nres_rel›
by (fastforce simp: refine_rel_defs nres_rel_def pw_ref_iff)
method match_spec =
(match conclusion in ‹(f, g) ∈ R› for f g R ⇒
‹print_term f; match premises in I[thin]: ‹(f, g) ∈ R'› for R'
⇒ ‹print_term R'; rule mem_set_trans[OF _ I]››)
method match_fun_rel =
((match conclusion in
‹_ → _ ⊆ _ → _› ⇒ ‹rule fun_rel_mono›
¦ ‹_ →⇩f _ ⊆ _ →⇩f _› ⇒ ‹rule fref_syn_invert›
¦ ‹⟨_⟩nres_rel ⊆ ⟨_⟩nres_rel› ⇒ ‹rule nres_rel_mono›
¦ ‹[_]⇩f _ → _ ⊆ [_]⇩f _ → _› ⇒ ‹rule fref_mono›
)+)
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]››)
subsection ‹More Notations›
abbreviation "uncurry2 f ≡ uncurry (uncurry f)"
abbreviation "curry2 f ≡ curry (curry f)"
abbreviation "uncurry3 f ≡ uncurry (uncurry2 f)"
abbreviation "curry3 f ≡ curry (curry2 f)"
abbreviation "uncurry4 f ≡ uncurry (uncurry3 f)"
abbreviation "curry4 f ≡ curry (curry3 f)"
abbreviation "uncurry5 f ≡ uncurry (uncurry4 f)"
abbreviation "curry5 f ≡ curry (curry4 f)"
abbreviation "uncurry6 f ≡ uncurry (uncurry5 f)"
abbreviation "curry6 f ≡ curry (curry5 f)"
abbreviation "uncurry7 f ≡ uncurry (uncurry6 f)"
abbreviation "curry7 f ≡ curry (curry6 f)"
abbreviation "uncurry8 f ≡ uncurry (uncurry7 f)"
abbreviation "curry8 f ≡ curry (curry7 f)"
abbreviation "uncurry9 f ≡ uncurry (uncurry8 f)"
abbreviation "curry9 f ≡ curry (curry8 f)"
abbreviation "uncurry10 f ≡ uncurry (uncurry9 f)"
abbreviation "curry10 f ≡ curry (curry9 f)"
abbreviation "uncurry11 f ≡ uncurry (uncurry10 f)"
abbreviation "curry11 f ≡ curry (curry10 f)"
abbreviation "uncurry12 f ≡ uncurry (uncurry11 f)"
abbreviation "curry12 f ≡ curry (curry11 f)"
abbreviation "uncurry13 f ≡ uncurry (uncurry12 f)"
abbreviation "curry13 f ≡ curry (curry12 f)"
abbreviation "uncurry14 f ≡ uncurry (uncurry13 f)"
abbreviation "curry14 f ≡ curry (curry13 f)"
abbreviation "uncurry15 f ≡ uncurry (uncurry14 f)"
abbreviation "curry15 f ≡ curry (curry14 f)"
abbreviation "uncurry16 f ≡ uncurry (uncurry15 f)"
abbreviation "curry16 f ≡ curry (curry15 f)"
abbreviation "uncurry17 f ≡ uncurry (uncurry16 f)"
abbreviation "curry17 f ≡ curry (curry16 f)"
abbreviation "uncurry18 f ≡ uncurry (uncurry17 f)"
abbreviation "curry18 f ≡ curry (curry17 f)"
abbreviation "uncurry19 f ≡ uncurry (uncurry18 f)"
abbreviation "curry19 f ≡ curry (curry18 f)"
abbreviation "uncurry20 f ≡ uncurry (uncurry19 f)"
abbreviation "curry20 f ≡ curry (curry19 f)"
abbreviation comp4 (infixl "oooo" 55) where "f oooo g ≡ λx. f ooo (g x)"
abbreviation comp5 (infixl "ooooo" 55) where "f ooooo g ≡ λx. f oooo (g x)"
abbreviation comp6 (infixl "oooooo" 55) where "f oooooo g ≡ λx. f ooooo (g x)"
abbreviation comp7 (infixl "ooooooo" 55) where "f ooooooo g ≡ λx. f oooooo (g x)"
abbreviation comp8 (infixl "oooooooo" 55) where "f oooooooo g ≡ λx. f ooooooo (g x)"
abbreviation comp9 (infixl "ooooooooo" 55) where "f ooooooooo g ≡ λx. f oooooooo (g x)"
abbreviation comp10 (infixl "oooooooooo" 55) where "f oooooooooo g ≡ λx. f ooooooooo (g x)"
abbreviation comp11 (infixl "o⇩1⇩1" 55) where "f o⇩1⇩1 g ≡ λx. f oooooooooo (g x)"
abbreviation comp12 (infixl "o⇩1⇩2" 55) where "f o⇩1⇩2 g ≡ λx. f o⇩1⇩1 (g x)"
abbreviation comp13 (infixl "o⇩1⇩3" 55) where "f o⇩1⇩3 g ≡ λx. f o⇩1⇩2 (g x)"
abbreviation comp14 (infixl "o⇩1⇩4" 55) where "f o⇩1⇩4 g ≡ λx. f o⇩1⇩3 (g x)"
abbreviation comp15 (infixl "o⇩1⇩5" 55) where "f o⇩1⇩5 g ≡ λx. f o⇩1⇩4 (g x)"
abbreviation comp16 (infixl "o⇩1⇩6" 55) where "f o⇩1⇩6 g ≡ λx. f o⇩1⇩5 (g x)"
abbreviation comp17 (infixl "o⇩1⇩7" 55) where "f o⇩1⇩7 g ≡ λx. f o⇩1⇩6 (g x)"
abbreviation comp18 (infixl "o⇩1⇩8" 55) where "f o⇩1⇩8 g ≡ λx. f o⇩1⇩7 (g x)"
abbreviation comp19 (infixl "o⇩1⇩9" 55) where "f o⇩1⇩9 g ≡ λx. f o⇩1⇩8 (g x)"
abbreviation comp20 (infixl "o⇩2⇩0" 55) where "f o⇩2⇩0 g ≡ λx. f o⇩1⇩9 (g x)"
notation
comp4 (infixl "∘∘∘" 55) and
comp5 (infixl "∘∘∘∘" 55) and
comp6 (infixl "∘∘∘∘∘" 55) and
comp7 (infixl "∘∘∘∘∘∘" 55) and
comp8 (infixl "∘∘∘∘∘∘∘" 55) and
comp9 (infixl "∘∘∘∘∘∘∘∘" 55) and
comp10 (infixl "∘∘∘∘∘∘∘∘∘" 55) and
comp11 (infixl "∘⇩1⇩1" 55) and
comp12 (infixl "∘⇩1⇩2" 55) and
comp13 (infixl "∘⇩1⇩3" 55) and
comp14 (infixl "∘⇩1⇩4" 55) and
comp15 (infixl "∘⇩1⇩5" 55) and
comp16 (infixl "∘⇩1⇩6" 55) and
comp17 (infixl "∘⇩1⇩7" 55) and
comp18 (infixl "∘⇩1⇩8" 55) and
comp19 (infixl "∘⇩1⇩9" 55) and
comp20 (infixl "∘⇩2⇩0" 55)
subsection ‹More Theorems for Refinement›
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 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
lemma fref_weaken_pre_weaken:
assumes "⋀x. P x ⟶ P' x"
assumes "(f,h) ∈ fref P' R S"
assumes ‹S ⊆ S'›
shows "(f,h) ∈ fref P R S'"
using assms unfolding fref_def by blast
lemma bind_rule_complete_RES: ‹(M ⤜ f ≤ RES Φ) = (M ≤ SPEC (λx. f x ≤ RES Φ))›
by (auto simp: pw_le_iff refine_pw_simps)
lemma fref_to_Down:
‹(f, g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ f x ≤ ⇓ B (g x'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry_left:
fixes f:: ‹'a ⇒ 'b ⇒ 'c nres› and
A::‹(('a × 'b) × 'd) set›
shows
‹(uncurry f, g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀a b x'. P x' ⟹ ((a, b), x') ∈ A ⟹ f a b ≤ ⇓ B (g x'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry:
‹(uncurry f, uncurry g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y ≤ ⇓ B (g x' y'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry2:
‹(uncurry2 f, uncurry2 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z'. P ((x', y'), z') ⟹ (((x, y), z), ((x', y'), z')) ∈ A⟹
f x y z ≤ ⇓ B (g x' y' z'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry2':
‹(uncurry2 f, uncurry2 g) ∈ A →⇩f ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z'. (((x, y), z), ((x', y'), z')) ∈ A ⟹
f x y z ≤ ⇓ B (g x' y' z'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry3:
‹(uncurry3 f, uncurry3 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z' a a'. P (((x', y'), z'), a') ⟹
((((x, y), z), a), (((x', y'), z'), a')) ∈ A ⟹
f x y z a ≤ ⇓ B (g x' y' z' a'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry4:
‹(uncurry4 f, uncurry4 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z' a a' b b'. P ((((x', y'), z'), a'), b') ⟹
(((((x, y), z), a), b), ((((x', y'), z'), a'), b')) ∈ A ⟹
f x y z a b ≤ ⇓ B (g x' y' z' a' b'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry5:
‹(uncurry5 f, uncurry5 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z' a a' b b' c c'. P (((((x', y'), z'), a'), b'), c') ⟹
((((((x, y), z), a), b), c), (((((x', y'), z'), a'), b'), c')) ∈ A ⟹
f x y z a b c ≤ ⇓ B (g x' y' z' a' b' c'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry6:
‹(uncurry6 f, uncurry6 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z' a a' b b' c c' d d'. P ((((((x', y'), z'), a'), b'), c'), d') ⟹
(((((((x, y), z), a), b), c), d), ((((((x', y'), z'), a'), b'), c'), d')) ∈ A ⟹
f x y z a b c d ≤ ⇓ B (g x' y' z' a' b' c' d'))›
unfolding fref_def uncurry_def nres_rel_def by auto
lemma fref_to_Down_curry7:
‹(uncurry7 f, uncurry7 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z' a a' b b' c c' d d' e e'. P (((((((x', y'), z'), a'), b'), c'), d'), e') ⟹
((((((((x, y), z), a), b), c), d), e), (((((((x', y'), z'), a'), b'), c'), d'), e')) ∈ A ⟹
f x y z a b c d e ≤ ⇓ B (g x' y' z' a' b' c' d' e'))›
unfolding fref_def uncurry_def nres_rel_def by auto
lemma fref_to_Down_explode:
‹(f a, g a) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' b. P x' ⟹ (x, x') ∈ A ⟹ b = a ⟹ f a x ≤ ⇓ B (g b x'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry_no_nres_Id:
‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨Id⟩nres_rel ⟹
(⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y = g x' y')›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_no_nres:
‹((RETURN o f), (RETURN o g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x'. P (x') ⟹ (x, x') ∈ A ⟹ (f x, g x') ∈ B)›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_curry_no_nres:
‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ (f x y, g x' y') ∈ B)›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma RES_RETURN_RES4:
‹SPEC Φ ⤜ (λ(T, T', T'', T'''). RETURN (f T T' T'' T''')) =
RES ((λ(a, b, c, d). f a b c d) ` {T. Φ T})›
using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c, d). f a b c d›]
apply (subst (asm)(2) split_prod_bound)
apply (subst (asm)(3) split_prod_bound)
apply (subst (asm)(4) split_prod_bound)
by auto
declare RETURN_as_SPEC_refine[refine2 del]
lemma fref_to_Down_unRET_uncurry_Id:
‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨Id⟩nres_rel ⟹
(⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y = (g x' y'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_unRET_uncurry:
‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ (f x y, g x' y') ∈ B)›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_unRET_Id:
‹((RETURN o f), (RETURN o g)) ∈ [P]⇩f A → ⟨Id⟩nres_rel ⟹
(⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ f x = (g x'))›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_unRET:
‹((RETURN o f), (RETURN o g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ (f x, g x') ∈ B)›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_unRET_uncurry2:
fixes f :: ‹'a ⇒ 'b ⇒ 'c ⇒ 'f›
and g :: ‹'a2 ⇒ 'b2 ⇒ 'c2 ⇒ 'g›
shows
‹(uncurry2 (RETURN ooo f), uncurry2 (RETURN ooo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2).
P ((x', y'), z') ⟹ (((x, y), z), ((x', y'), z')) ∈ A ⟹
(f x y z, g x' y' z') ∈ B)›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_unRET_uncurry3:
shows
‹(uncurry3 (RETURN oooo f), uncurry3 (RETURN oooo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2) a a'.
P (((x', y'), z'), a') ⟹ ((((x, y), z), a), (((x', y'), z'), a')) ∈ A ⟹
(f x y z a, g x' y' z' a') ∈ B)›
unfolding fref_def uncurry_def nres_rel_def
by auto
lemma fref_to_Down_unRET_uncurry4:
shows
‹(uncurry4 (RETURN ooooo f), uncurry4 (RETURN ooooo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2) a a' b b'.
P ((((x', y'), z'), a'), b') ⟹ (((((x, y), z), a), b), ((((x', y'), z'), a'), b')) ∈ A ⟹
(f x y z a b, g x' y' z' a' b') ∈ B)›
unfolding fref_def uncurry_def nres_rel_def
by auto
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 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
subsection ‹More declarations›
notation prod_rel_syn (infixl "×⇩f" 70)
lemma diff_add_mset_remove1: ‹NO_MATCH {#} N ⟹ M - add_mset a N = remove1_mset a (M - N)›
by auto
subsection ‹List relation›
lemma list_rel_take:
‹(ba, ab) ∈ ⟨A⟩list_rel ⟹ (take b ba, take b ab) ∈ ⟨A⟩list_rel›
by (auto simp: list_rel_def)
lemma list_rel_update':
fixes R
assumes rel: ‹(xs, ys) ∈ ⟨R⟩list_rel› and
h: ‹(bi, b) ∈ R›
shows ‹(list_update xs ba bi, list_update ys ba b) ∈ ⟨R⟩list_rel›
proof -
have [simp]: ‹(bi, b) ∈ R›
using h by auto
have ‹length xs = length ys›
using assms list_rel_imp_same_length by blast
then show ?thesis
using rel
by (induction xs ys arbitrary: ba rule: list_induct2) (auto split: nat.splits)
qed
lemma list_rel_in_find_correspondanceE:
assumes ‹(M, M') ∈ ⟨R⟩list_rel› and ‹L ∈ set M›
obtains L' where ‹(L, L') ∈ R› and ‹L' ∈ set M'›
using assms[unfolded in_set_conv_decomp] by (auto simp: list_rel_append1
elim!: list_relE3)
subsection ‹More Functions, Relations, and Theorems›
definition emptied_list :: ‹'a list ⇒ 'a list› where
‹emptied_list l = []›
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 order_class.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
subsubsection ‹Ghost parameters›
text ‹
This is a trick to recover from consumption of a variable (\<^term>‹𝒜⇩i⇩n›) that is passed as
argument and destroyed by the initialisation: We copy it as a zero-cost
(by creating a \<^term>‹()›), because we don't need it in the code and only in the specification.
This is a way to have ghost parameters, without having them: The parameter is replaced by \<^term>‹()›
and we hope that the compiler will do the right thing.
›
definition virtual_copy where
[simp]: ‹virtual_copy = id›
definition virtual_copy_rel where
‹virtual_copy_rel = {(c, b). c = ()}›
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 order_class.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
end