theory WB_More_IICF_SML
imports Refine_Imperative_HOL.IICF WB_More_Refinement WB_More_Refinement_List
begin
no_notation Sepref_Rules.fref ("[_]⇩f _ → _" [0,60,60] 60)
no_notation Sepref_Rules.freft ("_ →⇩f _" [60,60] 60)
no_notation prod_assn (infixr "×⇩a" 70)
notation prod_assn (infixr "*a" 70)
hide_const Autoref_Fix_Rel.CONSTRAINT IICF_List_Mset.list_mset_rel
lemma prod_assn_id_assn_destroy:
fixes R :: ‹_ ⇒ _ ⇒ assn›
shows ‹R⇧d *⇩a id_assn⇧d = (R *a id_assn)⇧d›
by (auto simp: hfprod_def prod_assn_def[abs_def] invalid_assn_def pure_def intro!: ext)
definition list_mset_assn where
"list_mset_assn A ≡ pure (list_mset_rel O ⟨the_pure A⟩mset_rel)"
declare list_mset_assn_def[symmetric,fcomp_norm_unfold]
lemma [safe_constraint_rules]: "is_pure (list_mset_assn A)" unfolding list_mset_assn_def by simp
lemma
shows list_mset_assn_add_mset_Nil:
‹list_mset_assn R (add_mset q Q) [] = false› and
list_mset_assn_empty_Cons:
‹list_mset_assn R {#} (x # xs) = false›
unfolding list_mset_assn_def list_mset_rel_def mset_rel_def pure_def p2rel_def
rel2p_def rel_mset_def br_def
by (sep_auto simp: Collect_eq_comp)+
lemma list_mset_assn_add_mset_cons_in:
assumes
assn: ‹A ⊨ list_mset_assn R N (ab # list)›
shows ‹∃ab'. (ab, ab') ∈ the_pure R ∧ ab' ∈# N ∧ A ⊨ list_mset_assn R (remove1_mset ab' N) (list)›
proof -
have H: ‹(∀x x'. (x' = x) = ((x', x) ∈ P')) ⟷ P' = Id› for P'
by (auto simp: the_pure_def)
have [simp]: ‹the_pure (λa c. ↑ (c = a)) = Id›
by (auto simp: the_pure_def H)
have [iff]: ‹(ab # list, y) ∈ list_mset_rel ⟷ y = add_mset ab (mset list)› for y ab list
by (auto simp: list_mset_rel_def br_def)
obtain N' xs where
N_N': ‹N = mset N'› and
‹mset xs = add_mset ab (mset list)› and
‹list_all2 (rel2p (the_pure R)) xs N'›
using assn by (cases A) (auto simp: list_mset_assn_def mset_rel_def p2rel_def rel_mset_def
rel2p_def)
then obtain N'' where
‹list_all2 (rel2p (the_pure R)) (ab # list) N''› and
‹mset N'' = mset N'›
using list_all2_reorder_left_invariance[of ‹rel2p (the_pure R)› xs N'
‹ab # list›, unfolded eq_commute[of ‹mset (ab # list)›]] by auto
then obtain n N''' where
n: ‹add_mset n (mset N''') = mset N''› and
‹(ab, n) ∈ the_pure R› and
‹list_all2 (rel2p (the_pure R)) list N'''›
by (auto simp: list_all2_Cons1 rel2p_def)
moreover have ‹n ∈ set N''›
using n unfolding mset.simps[symmetric] eq_commute[of ‹add_mset _ _›] apply -
by (drule mset_eq_setD) auto
ultimately have ‹(ab, n) ∈ the_pure R› and
‹n ∈ set N''› and
‹mset list = mset list› and
‹mset N''' = remove1_mset n (mset N'')› and
‹list_all2 (rel2p (the_pure R)) list N'''›
by (auto dest: mset_eq_setD simp: eq_commute[of ‹add_mset _ _›])
show ?thesis
unfolding list_mset_assn_def mset_rel_def p2rel_def rel_mset_def
list.rel_eq list_mset_rel_def
br_def N_N'
using assn ‹(ab, n) ∈ the_pure R› ‹n ∈ set N''› ‹mset N'' = mset N'›
‹list_all2 (rel2p (the_pure R)) list N'''›
‹mset N'' = mset N'› ‹mset N''' = remove1_mset n (mset N'')›
by (cases A) (auto simp: list_mset_assn_def mset_rel_def p2rel_def rel_mset_def
add_mset_eq_add_mset list.rel_eq
intro!: exI[of _ n]
dest: mset_eq_setD)
qed
lemma list_mset_assn_empty_nil: ‹list_mset_assn R {#} [] = emp›
by (auto simp: list_mset_assn_def list_mset_rel_def mset_rel_def
br_def p2rel_def rel2p_def Collect_eq_comp rel_mset_def
pure_def)
lemma is_Nil_is_empty[sepref_fr_rules]:
‹(return o is_Nil, RETURN o Multiset.is_empty) ∈ (list_mset_assn R)⇧k →⇩a bool_assn›
apply sepref_to_hoare
apply (rename_tac x xi)
apply (case_tac x)
by (sep_auto simp: Multiset.is_empty_def list_mset_assn_empty_Cons list_mset_assn_add_mset_Nil
split: list.splits)+
lemma list_all2_remove:
assumes
uniq: ‹IS_RIGHT_UNIQUE (p2rel R)› ‹IS_LEFT_UNIQUE (p2rel R)› and
Ra: ‹R a aa› and
all: ‹list_all2 R xs ys›
shows
‹∃xs'. mset xs' = remove1_mset a (mset xs) ∧
(∃ys'. mset ys' = remove1_mset aa (mset ys) ∧ list_all2 R xs' ys')›
using all
proof (induction xs ys rule: list_all2_induct)
case Nil
then show ?case by auto
next
case (Cons x y xs ys) note IH = this(3) and p = this(1, 2)
have ax: ‹{#a, x#} = {#x, a#}›
by auto
have rem1: ‹remove1_mset a (remove1_mset x M) = remove1_mset x (remove1_mset a M)› for M
by (auto simp: ax)
have H: ‹x = a ⟷ y = aa›
using uniq Ra p unfolding single_valued_def IS_LEFT_UNIQUE_def p2rel_def by blast
obtain xs' ys' where
‹mset xs' = remove1_mset a (mset xs)› and
‹mset ys' = remove1_mset aa (mset ys)› and
‹list_all2 R xs' ys'›
using IH p by auto
then show ?case
apply (cases ‹x ≠ a›)
subgoal
using p
by (auto intro!: exI[of _ ‹x#xs'›] exI[of _ ‹y#ys'›]
simp: diff_add_mset_remove1 rem1 add_mset_remove_trivial_If in_remove1_mset_neq H
simp del: diff_diff_add_mset)
subgoal
using p
by (fastforce simp: diff_add_mset_remove1 rem1 add_mset_remove_trivial_If in_remove1_mset_neq
remove_1_mset_id_iff_notin H
simp del: diff_diff_add_mset)
done
qed
lemma remove1_remove1_mset:
assumes uniq: ‹IS_RIGHT_UNIQUE R› ‹IS_LEFT_UNIQUE R›
shows ‹(uncurry (RETURN oo remove1), uncurry (RETURN oo remove1_mset)) ∈
R ×⇩r (list_mset_rel O ⟨R⟩ mset_rel) →⇩f
⟨list_mset_rel O ⟨R⟩ mset_rel⟩ nres_rel›
using list_all2_remove[of ‹rel2p R›] assms
by (intro frefI nres_relI) (fastforce simp: list_mset_rel_def br_def mset_rel_def p2rel_def
rel2p_def[abs_def] rel_mset_def Collect_eq_comp)
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)
lemma snd_hnr_pure:
‹CONSTRAINT is_pure B ⟹ (return ∘ snd, RETURN ∘ snd) ∈ A⇧d *⇩a B⇧k →⇩a B›
apply sepref_to_hoare
apply sep_auto
by (metis SLN_def SLN_left assn_times_comm ent_pure_pre_iff_sng ent_refl ent_star_mono
ent_true is_pure_assn_def is_pure_iff_pure_assn)
text ‹
This theorem is useful to debug situation where sepref is not able to synthesize a program (with
the ``[[unify\_trace\_failure]]'' to trace what fails in rule rule and the \<^text>‹to_hnr› to
ensure the theorem has the correct form).
›
lemma Pair_hnr: ‹(uncurry (return oo (λa b. Pair a b)), uncurry (RETURN oo (λa b. Pair a b))) ∈
A⇧d *⇩a B⇧d →⇩a prod_assn A B›
by sepref_to_hoare sep_auto
text ‹This version works only for ∗‹pure› refinement relations:›
lemma the_hnr_keep:
‹CONSTRAINT is_pure A ⟹ (return o the, RETURN o the) ∈ [λD. D ≠ None]⇩a (option_assn A)⇧k → A›
using pure_option[of A]
by sepref_to_hoare
(sep_auto simp: option_assn_alt_def is_pure_def split: option.splits)
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_mset_assn_pure_conv:
‹list_mset_assn (pure R) = pure (⟨R⟩list_rel_mset_rel)›
apply (intro ext)
using list_all2_reorder_left_invariance
by (fastforce
simp: list_rel_mset_rel_def list_mset_assn_def
mset_rel_def rel2p_def[abs_def] rel_mset_def p2rel_def
list_mset_rel_def[abs_def] Collect_eq_comp br_def
list_rel_def Collect_eq_comp_right
intro!: arg_cong[of _ _ ‹λb. pure b _ _›])
lemma list_assn_list_mset_rel_eq_list_mset_assn:
assumes p: ‹is_pure R›
shows ‹hr_comp (list_assn R) list_mset_rel = list_mset_assn R›
proof -
define R' where ‹R' = the_pure R›
then have R: ‹R = pure R'›
using p by auto
show ?thesis
apply (auto simp: list_mset_assn_def
list_assn_pure_conv
relcomp.simps hr_comp_pure mset_rel_def br_def
p2rel_def rel2p_def[abs_def] rel_mset_def R list_mset_rel_def list_rel_def)
using list_all2_reorder_left_invariance by fastforce
qed
lemma id_ref: ‹(return o id, RETURN o id) ∈ R⇧d →⇩a R›
by sepref_to_hoare sep_auto
text ‹This functions deletes all elements of a resizable array, without resizing it.›
definition emptied_arl :: ‹'a array_list ⇒ 'a array_list› where
‹emptied_arl = (λ(a, n). (a, 0))›
lemma emptied_arl_refine[sepref_fr_rules]:
‹(return o emptied_arl, RETURN o emptied_list) ∈ (arl_assn R)⇧d →⇩a arl_assn R›
unfolding emptied_arl_def emptied_list_def
by sepref_to_hoare (sep_auto simp: arl_assn_def hr_comp_def is_array_list_def)
lemma bool_assn_alt_def: ‹bool_assn a b = ↑ (a = b)›
unfolding pure_def by auto
lemma nempty_list_mset_rel_iff: ‹M ≠ {#} ⟹
(xs, M) ∈ list_mset_rel ⟷ (xs ≠ [] ∧ hd xs ∈# M ∧
(tl xs, remove1_mset (hd xs) M) ∈ list_mset_rel)›
by (cases xs) (auto simp: list_mset_rel_def br_def dest!: multi_member_split)
abbreviation ghost_assn where
‹ghost_assn ≡ hr_comp unit_assn virtual_copy_rel›
lemma [sepref_fr_rules]:
‹(return o (λ_. ()), RETURN o virtual_copy) ∈ R⇧k →⇩a ghost_assn›
by sepref_to_hoare (sep_auto simp: virtual_copy_rel_def)
lemma id_mset_list_assn_list_mset_assn:
assumes ‹CONSTRAINT is_pure R›
shows ‹(return o id, RETURN o mset) ∈ (list_assn R)⇧d →⇩a list_mset_assn R›
proof -
obtain R' where R: ‹R = pure R'›
using assms is_pure_conv unfolding CONSTRAINT_def by blast
then have R': ‹the_pure R = R'›
unfolding R by auto
show ?thesis
apply (subst R)
apply (subst list_assn_pure_conv)
apply sepref_to_hoare
by (sep_auto simp: list_mset_assn_def R' pure_def list_mset_rel_def mset_rel_def
p2rel_def rel2p_def[abs_def] rel_mset_def br_def Collect_eq_comp list_rel_def)
qed
subsection ‹Sorting›
text ‹Remark that we do not ∗‹prove› that the sorting in correct, since we do not care about the
correctness, only the fact that it is reordered. (Based on wikipedia's algorithm.)
Typically \<^term>‹R› would be \<^term>‹(<)››
definition insert_sort_inner :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a list ⇒ nat ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ 'a list nres› where
‹insert_sort_inner R f xs i = do {
(j, ys) ← WHILE⇩T⇗λ(j, ys). j ≥ 0 ∧ mset xs = mset ys ∧ j < length ys⇖
(λ(j, ys). j > 0 ∧ R (f ys j) (f ys (j - 1)))
(λ(j, ys). do {
ASSERT(j < length ys);
ASSERT(j > 0);
ASSERT(j-1 < length ys);
let xs = swap ys j (j - 1);
RETURN (j-1, xs)
}
)
(i, xs);
RETURN ys
}›
lemma ‹RETURN [Suc 0, 2, 0] = insert_sort_inner (<) (λremove n. remove ! n) [2::nat, 1, 0] 1›
by (simp add: WHILEIT_unfold insert_sort_inner_def swap_def)
definition insert_sort :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a list ⇒ nat ⇒ 'b) ⇒ 'a list ⇒ 'a list nres› where
‹insert_sort R f xs = do {
(i, ys) ← WHILE⇩T⇗λ(i, ys). (ys = [] ∨ i ≤ length ys) ∧ mset xs = mset ys⇖
(λ(i, ys). i < length ys)
(λ(i, ys). do {
ASSERT(i < length ys);
ys ← insert_sort_inner R f ys i;
RETURN (i+1, ys)
})
(1, xs);
RETURN ys
}›
lemma insert_sort_inner:
‹(uncurry (insert_sort_inner R f), uncurry (λm m'. reorder_list m' m)) ∈
[λ(xs, i). i < length xs]⇩f ⟨Id:: ('a × 'a) set⟩list_rel ×⇩r nat_rel → ⟨Id⟩ nres_rel›
unfolding insert_sort_inner_def uncurry_def reorder_list_def
apply (intro frefI nres_relI)
apply clarify
apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i, _). i)›])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto dest: mset_eq_length)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
lemma insert_sort_reorder_list:
‹(insert_sort R f, reorder_list vm) ∈ ⟨Id⟩list_rel →⇩f ⟨Id⟩ nres_rel›
proof -
have H: ‹ba < length aa ⟹ insert_sort_inner R f aa ba ≤ SPEC (λm'. mset m' = mset aa)›
for ba aa
using insert_sort_inner[unfolded fref_def nres_rel_def reorder_list_def, simplified]
by fast
show ?thesis
unfolding insert_sort_def reorder_list_def
apply (intro frefI nres_relI)
apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i, ys). length ys - i)›] H)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto dest: mset_eq_length)
subgoal by auto
subgoal by (auto dest!: mset_eq_length)
subgoal by auto
done
qed
definition arl_replicate where
"arl_replicate init_cap x ≡ do {
let n = max init_cap minimum_capacity;
a ← Array.new n x;
return (a,init_cap)
}"
definition ‹op_arl_replicate = op_list_replicate›
lemma arl_fold_custom_replicate:
‹replicate = op_arl_replicate›
unfolding op_arl_replicate_def op_list_replicate_def ..
lemma list_replicate_arl_hnr[sepref_fr_rules]:
assumes p: ‹CONSTRAINT is_pure R›
shows ‹(uncurry arl_replicate, uncurry (RETURN oo op_arl_replicate)) ∈ nat_assn⇧k *⇩a R⇧k →⇩a arl_assn R›
proof -
obtain R' where
R'[symmetric]: ‹R' = the_pure R› and
R_R': ‹R = pure R'›
using assms by fastforce
have [simp]: ‹pure R' b bi = ↑((bi, b) ∈ R')› for b bi
by (auto simp: pure_def)
have [simp]: ‹min a (max a 16) = a› for a :: nat
by auto
show ?thesis
using assms unfolding op_arl_replicate_def
by sepref_to_hoare
(sep_auto simp: arl_replicate_def arl_assn_def hr_comp_def R' R_R' list_rel_def
is_array_list_def minimum_capacity_def
intro!: list_all2_replicate)
qed
lemma option_bool_assn_direct_eq_hnr:
‹(uncurry (return oo (=)), uncurry (RETURN oo (=))) ∈
(option_assn bool_assn)⇧k *⇩a (option_assn bool_assn)⇧k →⇩a bool_assn›
by sepref_to_hoare (sep_auto simp: option_assn_alt_def split:option.splits)
text ‹This function does not change the size of the underlying array.›
definition take1 where
‹take1 xs = take 1 xs›
lemma take1_hnr[sepref_fr_rules]:
‹(return o (λ(a, _). (a, 1::nat)), RETURN o take1) ∈ [λxs. xs ≠ []]⇩a (arl_assn R)⇧d → arl_assn R›
apply sepref_to_hoare
apply (sep_auto simp: arl_assn_def hr_comp_def take1_def list_rel_def
is_array_list_def)
apply (case_tac b; case_tac x; case_tac l')
apply (auto)
done
text ‹The following two abbreviation are variants from \<^term>‹uncurry4› and
\<^term>‹uncurry6›. The problem is that \<^term>‹uncurry2 (uncurry2 f)› and
\<^term>‹uncurry (uncurry3 f)› are the same term, but only the latter is folded
to \<^term>‹uncurry4›.›
abbreviation uncurry4' where
"uncurry4' f ≡ uncurry2 (uncurry2 f)"
abbreviation uncurry6' where
"uncurry6' f ≡ uncurry2 (uncurry4' f)"
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 list_assn_map_list_assn: ‹list_assn g (map f x) xi = list_assn (λa c. g (f a) c) x xi›
apply (induction x arbitrary: xi)
subgoal by auto
subgoal for a x xi
by (cases xi) auto
done
lemma hfref_imp2: "(⋀x y. S x y ⟹⇩t S' x y) ⟹ [P]⇩a RR → S ⊆ [P]⇩a RR → S'"
apply clarsimp
apply (erule hfref_cons)
apply (simp_all add: hrp_imp_def)
done
lemma hr_comp_mono_entails: ‹B ⊆ C ⟹ hr_comp a B x y ⟹⇩A hr_comp a C x y›
unfolding hr_comp_def entails_def
by auto
lemma hfref_imp_mono_result:
"B ⊆ C ⟹ [P]⇩a RR → hr_comp a B ⊆ [P]⇩a RR → hr_comp a C"
unfolding hfref_def hn_refine_def
apply clarify
subgoal for aa b c aaa
apply (rule cons_post_rule[of _ _
‹λr. snd RR aaa c * (∃⇩Ax. hr_comp a B x r * ↑ (RETURN x ≤ b aaa)) * true›])
apply (solves auto)
using hr_comp_mono_entails[of B C a ]
apply (auto intro!: ent_ex_preI)
apply (rule_tac x=xa in ent_ex_postI)
apply (auto intro!: ent_star_mono ac_simps)
done
done
lemma hfref_imp_mono_result2:
"(⋀x. P L x ⟹ B L ⊆ C L) ⟹ [P L]⇩a RR → hr_comp a (B L) ⊆ [P L]⇩a RR → hr_comp a (C L)"
unfolding hfref_def hn_refine_def
apply clarify
subgoal for aa b c aaa
apply (rule cons_post_rule[of _ _
‹λr. snd RR aaa c * (∃⇩Ax. hr_comp a (B L) x r * ↑ (RETURN x ≤ b aaa)) * true›])
apply (solves auto)
using hr_comp_mono_entails[of ‹B L› ‹C L› a ]
apply (auto intro!: ent_ex_preI)
apply (rule_tac x=xa in ent_ex_postI)
apply (auto intro!: ent_star_mono ac_simps)
done
done
lemma ex_assn_up_eq2: ‹(∃⇩Aba. f ba * ↑ (ba = c)) = (f c)›
by (simp add: ex_assn_def)
lemma ex_assn_pair_split: ‹(∃⇩Ab. P b) = (∃⇩Aa b. P (a, b))›
by (subst ex_assn_def, subst (1) ex_assn_def, auto)+
lemma ex_assn_swap: ‹(∃⇩Aa b. P a b) = (∃⇩Ab a. P a b)›
by (meson ent_ex_postI ent_ex_preI ent_iffI ent_refl)
lemma ent_ex_up_swap: ‹(∃⇩Aaa. ↑ (P aa)) = (↑(∃aa. P aa))›
by (smt ent_ex_postI ent_ex_preI ent_iffI ent_pure_pre_iff ent_refl mult.left_neutral)
lemma ex_assn_def_pure_eq_middle3:
‹(∃⇩Aba b bb. f b ba bb * ↑ (ba = h b bb) * P b ba bb) = (∃⇩Ab bb. f b (h b bb) bb * P b (h b bb) bb)›
‹(∃⇩Ab ba bb. f b ba bb * ↑ (ba = h b bb) * P b ba bb) = (∃⇩Ab bb. f b (h b bb) bb * P b (h b bb) bb)›
‹(∃⇩Ab bb ba. f b ba bb * ↑ (ba = h b bb) * P b ba bb) = (∃⇩Ab bb. f b (h b bb) bb * P b (h b bb) bb)›
‹(∃⇩Aba b bb. f b ba bb * ↑ (ba = h b bb ∧ Q b ba bb)) = (∃⇩Ab bb. f b (h b bb) bb * ↑(Q b (h b bb) bb))›
‹(∃⇩Ab ba bb. f b ba bb * ↑ (ba = h b bb ∧ Q b ba bb)) = (∃⇩Ab bb. f b (h b bb) bb * ↑(Q b (h b bb) bb))›
‹(∃⇩Ab bb ba. f b ba bb * ↑ (ba = h b bb ∧ Q b ba bb)) = (∃⇩Ab bb. f b (h b bb) bb * ↑(Q b (h b bb) bb))›
by (subst ex_assn_def, subst (3) ex_assn_def, auto)+
lemma ex_assn_def_pure_eq_middle2:
‹(∃⇩Aba b. f b ba * ↑ (ba = h b) * P b ba) = (∃⇩Ab . f b (h b) * P b (h b))›
‹(∃⇩Ab ba. f b ba * ↑ (ba = h b) * P b ba) = (∃⇩Ab . f b (h b) * P b (h b))›
‹(∃⇩Ab ba. f b ba * ↑ (ba = h b ∧ Q b ba)) = (∃⇩Ab. f b (h b) * ↑(Q b (h b)))›
‹(∃⇩A ba b. f b ba * ↑ (ba = h b ∧ Q b ba)) = (∃⇩Ab. f b (h b) * ↑(Q b (h b)))›
by (subst ex_assn_def, subst (2) ex_assn_def, auto)+
lemma ex_assn_skip_first2:
‹(∃⇩Aba bb. f bb * ↑(P ba bb)) = (∃⇩Abb. f bb * ↑(∃ba. P ba bb))›
‹(∃⇩Abb ba. f bb * ↑(P ba bb)) = (∃⇩Abb. f bb * ↑(∃ba. P ba bb))›
apply (subst ex_assn_swap)
by (subst ex_assn_def, subst (2) ex_assn_def, auto)+
lemma fr_refl': ‹A ⟹⇩A B ⟹ C * A ⟹⇩A C * B›
unfolding assn_times_comm[of C]
by (rule Automation.fr_refl)
lemma hrp_comp_Id2[simp]: ‹hrp_comp A Id = A›
unfolding hrp_comp_def by auto
lemma hn_ctxt_prod_assn_prod:
‹hn_ctxt (R *a S) (a, b) (a', b') = hn_ctxt R a a' * hn_ctxt S b b'›
unfolding hn_ctxt_def
by auto
lemma hfref_weaken_change_pre:
assumes "(f,h) ∈ hfref P R S"
assumes "⋀x. P x ⟹ (fst R x, snd R x) = (fst R' x, snd R' x)"
assumes "⋀y x. S y x ⟹⇩t S' y x"
shows "(f,h) ∈ hfref P R' S'"
proof -
have ‹(f,h) ∈ hfref P R' S›
using assms
by (auto simp: hfref_def)
then show ?thesis
using hfref_imp2[of S S' P R'] assms(3) by auto
qed
lemma norm_RETURN_o[to_hnr_post]:
"⋀f. (RETURN oooo f)$x$y$z$a = (RETURN$(f$x$y$z$a))"
"⋀f. (RETURN ooooo f)$x$y$z$a$b = (RETURN$(f$x$y$z$a$b))"
"⋀f. (RETURN oooooo f)$x$y$z$a$b$c = (RETURN$(f$x$y$z$a$b$c))"
"⋀f. (RETURN ooooooo f)$x$y$z$a$b$c$d = (RETURN$(f$x$y$z$a$b$c$d))"
"⋀f. (RETURN oooooooo f)$x$y$z$a$b$c$d$e = (RETURN$(f$x$y$z$a$b$c$d$e))"
"⋀f. (RETURN ooooooooo f)$x$y$z$a$b$c$d$e$g = (RETURN$(f$x$y$z$a$b$c$d$e$g))"
"⋀f. (RETURN oooooooooo f)$x$y$z$a$b$c$d$e$g$h= (RETURN$(f$x$y$z$a$b$c$d$e$g$h))"
"⋀f. (RETURN ∘⇩1⇩1 f)$x$y$z$a$b$c$d$e$g$h$i= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i))"
"⋀f. (RETURN ∘⇩1⇩2 f)$x$y$z$a$b$c$d$e$g$h$i$j= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j))"
"⋀f. (RETURN ∘⇩1⇩3 f)$x$y$z$a$b$c$d$e$g$h$i$j$l= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l))"
"⋀f. (RETURN ∘⇩1⇩4 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m))"
"⋀f. (RETURN ∘⇩1⇩5 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n))"
"⋀f. (RETURN ∘⇩1⇩6 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p= (RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p))"
"⋀f. (RETURN ∘⇩1⇩7 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r=
(RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r))"
"⋀f. (RETURN ∘⇩1⇩8 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s=
(RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s))"
"⋀f. (RETURN ∘⇩1⇩9 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t=
(RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t))"
"⋀f. (RETURN ∘⇩2⇩0 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u=
(RETURN$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u))"
by auto
lemma norm_return_o[to_hnr_post]:
"⋀f. (return oooo f)$x$y$z$a = (return$(f$x$y$z$a))"
"⋀f. (return ooooo f)$x$y$z$a$b = (return$(f$x$y$z$a$b))"
"⋀f. (return oooooo f)$x$y$z$a$b$c = (return$(f$x$y$z$a$b$c))"
"⋀f. (return ooooooo f)$x$y$z$a$b$c$d = (return$(f$x$y$z$a$b$c$d))"
"⋀f. (return oooooooo f)$x$y$z$a$b$c$d$e = (return$(f$x$y$z$a$b$c$d$e))"
"⋀f. (return ooooooooo f)$x$y$z$a$b$c$d$e$g = (return$(f$x$y$z$a$b$c$d$e$g))"
"⋀f. (return oooooooooo f)$x$y$z$a$b$c$d$e$g$h= (return$(f$x$y$z$a$b$c$d$e$g$h))"
"⋀f. (return ∘⇩1⇩1 f)$x$y$z$a$b$c$d$e$g$h$i= (return$(f$x$y$z$a$b$c$d$e$g$h$i))"
"⋀f. (return ∘⇩1⇩2 f)$x$y$z$a$b$c$d$e$g$h$i$j= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j))"
"⋀f. (return ∘⇩1⇩3 f)$x$y$z$a$b$c$d$e$g$h$i$j$l= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l))"
"⋀f. (return ∘⇩1⇩4 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m))"
"⋀f. (return ∘⇩1⇩5 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n))"
"⋀f. (return ∘⇩1⇩6 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p= (return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p))"
"⋀f. (return ∘⇩1⇩7 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r=
(return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r))"
"⋀f. (return ∘⇩1⇩8 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s=
(return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s))"
"⋀f. (return ∘⇩1⇩9 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t=
(return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t))"
"⋀f. (return ∘⇩2⇩0 f)$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u=
(return$(f$x$y$z$a$b$c$d$e$g$h$i$j$l$m$n$p$r$s$t$u))"
by auto
lemma list_rel_update:
fixes R :: ‹'a ⇒ 'b :: {heap}⇒ assn›
assumes rel: ‹(xs, ys) ∈ ⟨the_pure R⟩list_rel› and
h: ‹h ⊨ A * R b bi› and
p: ‹is_pure R›
shows ‹(list_update xs ba bi, list_update ys ba b) ∈ ⟨the_pure R⟩list_rel›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have [simp]: ‹(bi, b) ∈ the_pure R›
using h p by (auto simp: mod_star_conv R R')
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
end