Theory IICF_DS_Interval_List
theory IICF_DS_Interval_List
imports "Isabelle_LLVM.IICF"
begin
lemma sort_key_empty_iff[simp]: "sort_key f xs = [] ⟷ xs=[]"
by (cases xs) auto
lemma Max_at_least_less_than[simp]: "l<h ⟹ Max {l..<h} = h-1" for l h :: nat
apply (subgoal_tac "(∀x∈{l..<h}. x ≤ h-1)")
by (auto intro: antisym)
lemma id_set_constraint_simps:
"IS_LEFT_UNIQUE Id"
"single_valued Id"
"(True ⟹ PROP Q) ≡ PROP Q"
by (auto simp: left_unique_id)
lemma hr_comp_elim_b_rel:
assumes "⋀s s'. rdomp A s ⟹ (s,s')∈R ⟹ Φ s'"
shows "hr_comp A (b_rel R Φ) = hr_comp A R"
unfolding hr_comp_def
apply (auto simp: fun_eq_iff sep_algebra_simps)
using assms unfolding rdomp_def by blast
definition "is_commutative f ≡ ∀a b. f a b = f b a"
lemma is_commutativeI[intro?]: "⟦ ⋀a b. f a b = f b a ⟧ ⟹ is_commutative f" by (auto simp: is_commutative_def)
lemma is_commutative_RETURN[simp]: "is_commutative (Refine_Basic.RETURN ∘∘ f) = is_commutative f"
by (auto simp: is_commutative_def)
lemmas is_comm_simps = is_commutative_RETURN True_implies_equals
lemma hfref_commute_op:
assumes R: "(uncurry opi, uncurry op) ∈ [P]⇩a [C]⇩c Ax⇩1 *⇩a Ax⇩2 →⇩d A [CP]⇩c"
assumes C: "is_commutative op"
shows "(uncurry (λx y. opi y x), uncurry op) ∈ [λ(a,b). P (b,a)]⇩a [λ(a,b). C (b,a)]⇩c Ax⇩2 *⇩a Ax⇩1 →⇩d (λ(a,b). A (b,a)) [λ(ai,bi) ri. CP (bi,ai) ri]⇩c"
apply (rule hfrefI)
apply (rule hn_refineI)
apply clarsimp
subgoal for ai bi a b
apply (rule cons_rule)
supply R' = R[THEN hfrefD, THEN hn_refineD, of "(b,a)" "(bi,ai)", simplified]
apply (rule R')
using C
apply (auto simp: is_commutative_def sep_algebra_simps)
apply (metis sep.mult_commute)
subgoal for r s x
apply (rule exI[where x=x])
apply auto
by (simp only: sep_conj_ac)
done
done
lemma hfref_ttnd_commute_op:
assumes R: "(uncurry opi, uncurry op) ∈ Ax⇩1 *⇩a Ax⇩2 →⇩a A"
assumes C: "is_commutative op"
shows "(uncurry (λx y. opi y x), uncurry op) ∈ Ax⇩2 *⇩a Ax⇩1 →⇩a A"
using hfref_commute_op[OF R C]
apply (rule hfref_cons)
by auto
lemma Un_is_commutative[simp]:
"is_commutative (∪)"
"is_commutative op_set_union"
"is_commutative mop_set_union"
by (auto simp: is_commutative_def)
lemma Inter_is_commutative[simp]:
"is_commutative (∩)"
"is_commutative op_set_inter"
"is_commutative mop_set_inter"
by (auto simp: is_commutative_def)
lemma Range_prod_eq: "Range (a ×⇩r b) = Range a × Range b"
apply auto
apply rule
apply (rule prod_relI)
.
lemma rdomp_al_assn_len_bound: "rdomp (al_assn' TYPE('l::len2) A) c ⟹ 4<LENGTH('l)"
unfolding al_assn_def arl_assn_def arl_assn'_def rdomp_def
apply (rule ccontr)
by (auto simp: hr_comp_def)
lemma param_card[param]:
assumes "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A"
shows "(card,card) ∈ ⟨A⟩set_rel → nat_rel"
apply (rule rel2pD)
unfolding rel2p
apply (rule card_transfer)
by (simp add: p2prop assms)
sepref_decl_op set_card: "card" :: "⟨A⟩set_rel → nat_rel" where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .
section "Interval Lists"
subsection ‹Additional set ADT operations›
sepref_decl_op set_range: "λl h. {l..<h}" :: "(Id::'a::ord rel) → (Id::'a rel) → ⟨Id::'a rel⟩set_rel" .
sepref_decl_op set_range_lb: "λl. {l..}" :: "(Id::'a::ord rel) → ⟨Id::'a rel⟩set_rel" .
sepref_decl_op set_union_disj: "λa b. (a∪b)" :: "[λ(a,b::'a set). a∩b={}]⇩f ⟨Id⟩set_rel ×⇩r ⟨Id⟩set_rel → ⟨Id::'a rel⟩set_rel" by simp
sepref_decl_op set_incr_elems: "λn s. (+)n`s" :: "(Id::'a::plus rel) → ⟨Id::'a rel⟩set_rel → ⟨Id::'a rel⟩set_rel" .
lemma pat_set[def_pat_rules]:
"atLeastLessThan$l$h ≡ op_set_range$l$h"
"atLeast$l ≡ op_set_range_lb$l"
by auto
lemma Un_disj_is_commutative[simp]:
"is_commutative op_set_union_disj"
"is_commutative mop_set_union_disj"
by (auto intro!: is_commutativeI simp: Un_commute Int_commute)
term mop_set_empty
definition [simp]: "mop_set_rm_subset s ≡ doN { ASSERT (s≠{}); SPEC (λ(s⇩1,s⇩2). s=s⇩1∪s⇩2 ∧ s⇩1∩s⇩2={} ∧ s⇩1≠{}) }"
sepref_register mop_set_rm_subset
definition [simp]: "mop_set_split_card n s ≡ doN { ASSERT (s≠{} ∧ finite s ∧ n ≤ card s); SPEC (λ(s⇩1,s⇩2). s=s⇩1∪s⇩2 ∧ s⇩1∩s⇩2={} ∧ card s⇩1 = n ) }"
sepref_register mop_set_split_card
subsection ‹Intermediate Level DS›
subsubsection ‹Closed Intervals›
type_synonym iv = "nat × nat"
definition iv_α :: "iv ⇒ nat set" where "iv_α ≡ λ(l,h). {l..<h}"
definition "iv_rel ≡ br iv_α (λ_. True)"
definition iv_range :: "nat ⇒ nat ⇒ iv" where "iv_range l h ≡ (l,h)"
definition iv_is_empty :: "iv ⇒ bool" where "iv_is_empty ≡ λ(l,h). l≥h"
definition iv_inter :: "iv ⇒ iv ⇒ iv" where "iv_inter ≡ λ(l⇩1,h⇩1) (l⇩2,h⇩2). (max l⇩1 l⇩2, min h⇩1 h⇩2)"
definition iv_card :: "iv ⇒ nat" where "iv_card ≡ λ(l,h). if h<l then 0 else h-l"
definition "iv_split_card ≡ λn (l,h). doN {
ASSERT (l+n ≤ h);
RETURN ((l,l+n), (l+n,h))
}"
definition iv_incr_elems where "iv_incr_elems ≡ λn (l,h). if l<h then (l+n, h+n) else (l,h)"
context
notes [simp] = iv_rel_def in_br_conv iv_α_def
begin
lemma iv_range_refine: "(iv_range,op_set_range) ∈ Id → Id → iv_rel"
by (auto simp: iv_range_def)
lemma iv_is_empty_refine: "(iv_is_empty, op_set_is_empty) ∈ iv_rel → bool_rel"
by (auto simp: iv_is_empty_def)
lemma iv_inter_refine: "(iv_inter, op_set_inter) ∈ iv_rel → iv_rel → iv_rel"
by (auto simp: iv_inter_def)
lemma iv_card_refine: "(iv_card, op_set_card) ∈ iv_rel → nat_rel"
by (auto simp: iv_card_def)
lemma iv_incr_elems_refine: "(iv_incr_elems, op_set_incr_elems) ∈ nat_rel → iv_rel → iv_rel"
by (auto simp: iv_incr_elems_def)
lemma iv_α_finite[simp,intro!]: "finite (iv_α iv)" by (cases iv) auto
end
lemma iv_split_card_refine: "(iv_split_card, mop_set_split_card) ∈ nat_rel → iv_rel → ⟨iv_rel ×⇩r iv_rel⟩nres_rel"
unfolding iv_split_card_def
apply clarsimp
apply (refine_vcg RETURN_SPEC_refine)
unfolding iv_rel_def
by (auto simp: in_br_conv iv_α_def)
subsubsection ‹Open Intervals›
definition "iv_lb_rel ≡ { (l,{l..}) |l. True }"
lemma iv_lb_refine: "(id,op_set_range_lb) ∈ Id → iv_lb_rel"
by (auto simp: iv_lb_rel_def)
definition "iv_inter_lb ≡ λl (l',h'). (max l l', h')"
lemma iv_inter_lb_refine: "(iv_inter_lb, op_set_inter) ∈ iv_lb_rel → iv_rel → iv_rel"
by (auto simp: iv_inter_lb_def iv_lb_rel_def iv_rel_def in_br_conv iv_α_def)
subsubsection ‹Interval Lists›
type_synonym ivl = "nat set list"
definition ivl_α :: "ivl ⇒ nat set" where "ivl_α ivl = ⋃( set ivl )"
locale ivl_invar =
fixes ivl :: ivl
assumes distinct: "distinct ivl"
assumes non_empty: "{}∉set ivl"
assumes finite: "iv∈set ivl ⟹ finite iv"
assumes non_overlapping: "⟦i⇩1∈set ivl; i⇩2∈set ivl; i⇩1≠i⇩2⟧ ⟹ i⇩1 ∩ i⇩2 = {}"
begin
lemma in_set_ivlsD: "⟦ iv∈set ivl ⟧ ⟹ iv ⊆ ivl_α ivl ∧ iv≠{}"
using non_empty
by (auto simp: ivl_α_def)
lemma ivl_α_finite[simp, intro!]: "finite (ivl_α ivl)"
using finite unfolding ivl_α_def
by blast
lemma finite_Un_ivl[simp, intro!]: "finite (⋃ (set ivl))"
using ivl_α_def ivl_α_finite by presburger
end
lemmas [simp, intro] = ivl_invar.ivl_α_finite
definition "ivl_rel ≡ br ivl_α ivl_invar"
text ‹We start with defining properties of the refinement relation wrt lists.
These will later be used to prove the actual refinement lemmas
›
lemma ivl_α_empty_list[simp]: "ivl_α [] = {}" by (simp add: ivl_α_def)
lemma ivl_α_Cons[simp]: "ivl_α (iv#ivls) = iv ∪ ivl_α ivls"
by (auto simp: ivl_α_def)
lemma ivl_α_append[simp]: "ivl_α (ivl⇩1@ivl⇩2) = ivl_α ivl⇩1 ∪ ivl_α ivl⇩2"
by (auto simp: ivl_α_def)
lemma in_ivl_α_conv: "x∈ivl_α ivl ⟷ (∃iv∈set ivl. x∈iv)"
unfolding ivl_α_def
by (auto)
lemma iv_dj_ivl_α_conv: "s ∩ ivl_α ivl = {} ⟷ (∀s'∈set ivl. s ∩ s' = {})"
by (auto 0 3 simp: in_ivl_α_conv)
lemma in_set_ivls_α: "s∈set ivl ⟹ s ⊆ ivl_α ivl"
by (auto simp: in_set_conv_decomp)
lemma ivl_α_dj_conv: "ivl_α ivl⇩1 ∩ ivl_α ivl⇩2 = {} ⟷ (∀s∈set ivl⇩1. ∀s'∈set ivl⇩2. s ∩ s' = {})"
by (auto 0 4 simp: in_set_conv_decomp in_ivl_α_conv)
lemma ivl_invar_empty_list[simp]: "ivl_invar []" by (simp add: ivl_invar_def)
lemma ivl_invar_Cons[simp]: "ivl_invar (s#ivl) ⟷ s≠{} ∧ finite s ∧ s ∩ ivl_α ivl = {} ∧ ivl_invar ivl"
unfolding ivl_invar_def
apply (intro conjI iffI)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal apply (simp add: in_ivl_α_conv iv_dj_ivl_α_conv) by auto
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
subgoal by (auto 0 3 simp: in_ivl_α_conv iv_dj_ivl_α_conv)
done
lemma ivl_invar_append[simp]: "ivl_invar (ivls⇩1@ivls⇩2) ⟷ ivl_invar ivls⇩1 ∧ ivl_invar ivls⇩2 ∧ ivl_α ivls⇩1 ∩ ivl_α ivls⇩2 = {}"
unfolding ivl_invar_def
apply (intro conjI iffI)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by simp
subgoal by auto
subgoal by auto
subgoal by auto
subgoal apply (auto simp: in_ivl_α_conv) by (metis disjoint_iff)
subgoal by (fastforce simp: ivl_α_dj_conv)
subgoal by simp
subgoal by simp
subgoal by (simp add: ivl_α_dj_conv) fast
done
lemma ivl_invar_sort[simp]: "ivl_invar (sort_key f xs) = ivl_invar xs"
unfolding ivl_invar_def
by auto
text ‹
To later implement the list by dynamic arrays, we will need to show that the dynamic
array does not grow out of bounds, i.e., greater than what can be represented by its length field.
For this, we estimate the length of the list by the maximum set element it contains,
thus linking the length bound to the bound on set elements: if we use the same/lower bit-width
for storing the set elements as for the array's length counter, we can show that the bound will not be exceeded.
›
definition iv_maxl :: "nat set ⇒ nat" where "iv_maxl iv ≡ if iv={} ∨ infinite iv then 0 else 2 + Max iv"
definition "ivl_maxl ivl ≡ if ¬ivl_invar ivl then 0 else if ivl=[] then 1 else Max (iv_maxl`set ivl)"
lemma Max_UN_eq: "{}∉S ⟹ finite S ⟹ (∀s∈S. finite s) ⟹ Max (⋃S) = Max (Max`S)"
apply (cases "S={}"; simp)
by (smt (verit) Max_eq_iff Union_iff empty_iff finite_Union finite_imageI imageE image_eqI)
lemma Suc2_Max_commute: "⟦finite A; A ≠ {}⟧ ⟹ Suc (Suc (Max A)) = Max ((Suc o Suc) ` A)"
by (simp add: Inf.INF_image mono_Max_commute mono_Suc)
lemma ivl_maxl_alt: "ivl_maxl ivl = (if ¬ivl_invar ivl then 0 else if ivl=[] then 1 else 2 + Max (ivl_α ivl))"
unfolding ivl_maxl_def ivl_α_def iv_maxl_def
apply (auto simp: )
apply (simp add: image_constant_conv)
apply (intro allI impI conjI)
subgoal
apply (subgoal_tac "(set ivl ∩ {iv. iv ≠ {} ∧ finite iv}) = set ivl")
apply (simp add: Max_UN_eq ivl_invar.finite ivl_invar.non_empty Suc2_Max_commute image_image)
using ivl_invar.non_empty ivl_invar.finite
by blast
subgoal using ivl_invar.non_empty ivl_invar.finite by blast
done
lemma ivl_length_bound:
assumes "ivl_invar ivl"
shows "length ivl < ivl_maxl ivl"
using assms
proof (induction ivl rule: length_induct[case_names A])
case (A ivl)
interpret ivl_invar ivl by fact
show ?case proof (cases "ivl = []")
case True thus ?thesis by (simp add: ivl_maxl_def)
next
case False
with A.prems have "ivl_α ivl ≠ {}" by (auto simp: neq_Nil_conv)
hence
IN: "Max (ivl_α ivl) ∈ ivl_α ivl" and
MAX: "∀x∈ivl_α ivl. x ≤ Max (ivl_α ivl)"
by (auto simp: A.prems(1))
from IN obtain iv ivl⇩1 ivl⇩2 where IN_IV: "Max (ivl_α ivl) ∈ iv" and [simp]: "ivl = ivl⇩1@iv#ivl⇩2"
by (auto simp: in_ivl_α_conv in_set_conv_decomp)
from A.prems A.IH[rule_format, of "ivl⇩1@ivl⇩2"] have L: "length (ivl⇩1 @ ivl⇩2) < ivl_maxl (ivl⇩1 @ ivl⇩2)"
by auto
have "ivl_maxl (ivl⇩1 @ ivl⇩2) < ivl_maxl (ivl)"
using ‹ivl_invar ivl› IN_IV
apply (auto 0 0 simp add: ivl_maxl_alt neq_Nil_conv nat_less_le)
subgoal by (metis IntI UnCI UnE emptyE eq_Max_iff infinite_Un ivl_invar.ivl_α_finite)
subgoal by (metis IntI UnCI UnE emptyE eq_Max_iff infinite_Un ivl_invar.ivl_α_finite)
done
thus ?thesis using L by simp
qed
qed
lemma ivl_max_append: "ivl_invar (ivl@[iv]) ⟹ ivl_maxl (ivl@[iv]) = max (ivl_maxl ivl) (iv_maxl iv)"
unfolding ivl_maxl_alt iv_maxl_def
apply (clarsimp simp: neq_Nil_conv)
by (metis Max.union Un_empty ivl_α_Cons ivl_invar.ivl_α_finite ivl_invar_Cons)
lemma "(∀x∈s. x<N) ⟹ card s ≤ N" for s :: "nat set"
by (simp add: subsetI subset_eq_atLeast0_lessThan_card)
context ivl_invar begin
lemma set_ivl_inter_simps[simp]:
"set ivl ∩ {iv. iv = {} ∨ infinite iv} = {}"
"(set ivl ∩ {iv. iv ≠ {} ∧ finite iv}) = set ivl"
using finite non_empty
by auto
lemma ivl_max_notZ[simp]: "ivl_maxl ivl ≠ 0"
unfolding ivl_maxl_def
by (auto simp add: ivl_invar_axioms iv_maxl_def non_empty neq_Nil_conv Max_gr_iff)
lemma ivl_member_bound: "x∈ivl_α ivl ⟹ x+1<ivl_maxl ivl"
unfolding ivl_α_def ivl_maxl_def iv_maxl_def
apply (auto simp: ivl_invar_axioms Max_gr_iff)
by (metis Max_less_iff all_not_in_conv lessI local.finite)
lemma ivl_α_bound: "ivl_α ivl ⊆ {0..<ivl_maxl ivl - 1}"
using ivl_member_bound
by fastforce
lemma ivl_α_card_bound: "card (ivl_α ivl) < ivl_maxl ivl"
using ivl_α_bound
by (metis One_nat_def ivl_max_notZ less_imp_diff_less linorder_not_le minus_eq nat.simps(3) nat_neq_iff subset_eq_atLeast0_lessThan_card)
end
text ‹The actual implementations of the set operations›
definition "ivl_empty = []"
definition "ivl_is_empty ivls ⟷ ivls=[]"
definition "ivl_add iv ivl ≡ doN {
if (op_set_is_empty iv) then
RETURN ivl
else doN {
ASSERT (length ivl+1 < max (ivl_maxl ivl) (iv_maxl iv));
RETURN (ivl@[iv])
}
}"
definition "ivl_rm_subset (ivl::ivl) ≡ doN {
mop_list_pop_last ivl
}"
definition "ivl_card (ivl::ivl) ≡ doN {
nfoldli ivl (λ_. True) (λs acc. doN {
c ← mop_set_card s;
ASSERT (acc + c < ivl_maxl ivl);
RETURN (acc+c)
}) 0
}"
lemma ivl_empty_invar[simp]: "ivl_invar ivl_empty"
and ivl_empty_α[simp]: "ivl_α ivl_empty = {}"
unfolding ivl_α_def ivl_invar_def ivl_empty_def
by auto
lemma ivl_is_empty_α[simp]: "ivl_invar ivls ⟹ ivl_is_empty ivls ⟷ ivl_α ivls={}"
unfolding ivl_α_def ivl_invar_def ivl_is_empty_def
apply auto
by (metis ex_in_conv set_empty)
lemma ivl_empty_refine: "(ivl_empty,op_set_empty) ∈ ivl_rel"
by (auto simp: ivl_rel_def in_br_conv)
lemma ivl_is_empty_refine: "(ivl_is_empty, op_set_is_empty) ∈ ivl_rel → bool_rel"
by (auto simp: ivl_rel_def in_br_conv)
lemma m_ivl_add_bound_aux:
assumes "ivl_invar ivl" "iv≠{}" "iv ∩ ivl_α ivl = {}" "finite iv"
shows "Suc (length ivl) < max (ivl_maxl ivl) (iv_maxl iv)"
proof -
from assms have "ivl_invar (ivl@[iv])" by auto
from ivl_length_bound[OF this] ivl_max_append[OF this] show ?thesis by simp
qed
lemma ivl_add_refine: "(ivl_add, mop_set_union_disj) ∈ b_rel Id finite → ivl_rel → ⟨ivl_rel⟩nres_rel"
unfolding ivl_add_def
apply clarsimp
apply refine_vcg
by (auto simp: iv_rel_def ivl_rel_def in_br_conv m_ivl_add_bound_aux)
lemma ivl_rm_subset_refine: "(ivl_rm_subset,mop_set_rm_subset) ∈ ivl_rel → ⟨Id ×⇩r ivl_rel⟩nres_rel"
unfolding ivl_rm_subset_def mop_set_rm_subset_def
apply (refine_vcg RETURN_SPEC_refine)
apply (auto simp: ivl_rel_def in_br_conv) []
apply (clarsimp simp: ivl_rel_def in_br_conv)
subgoal for ivl by (cases ivl rule: rev_cases; auto)
done
lemma ivl_card_refine: "(ivl_card,mop_set_card) ∈ ivl_rel → ⟨nat_rel⟩nres_rel"
unfolding ivl_card_def
apply clarsimp
apply (refine_vcg RETURN_SPEC_refine nfoldli_rule[where I="λl1 l2 r. r = card (ivl_α l1)"])
apply (simp_all add: ivl_rel_def in_br_conv)
subgoal for ivl iv l1 l2 r
using ivl_invar.ivl_α_card_bound[of ivl]
by (auto simp: card_Un_disjoint)
apply (subst card_Un_disjoint)
apply auto
done
lemma ivl_max_bound_aux:
assumes "Suc 0 ≤ N"
assumes "⋀s. s∈set ivl ⟹ iv_maxl s ≤ N"
shows "ivl_maxl ivl ≤ N"
using assms
unfolding ivl_maxl_def
by auto
subsection ‹Refinement to LLVM›
context
fixes L
defines "L ≡ LENGTH ('l::len2)"
begin
subsubsection ‹Open and Closed Intervals›
private abbreviation (input) "sA ≡ snat_assn' TYPE('l)"
definition "iv_assn_raw ≡ sA ×⇩a sA"
private abbreviation (input) "ivA ≡ iv_assn_raw :: _ ⇒ 'l word × _ ⇒ _"
sepref_definition iv_range_impl [llvm_inline] is "uncurry (RETURN oo iv_range)" :: "sA⇧k*⇩asA⇧k →⇩a ivA"
unfolding iv_range_def iv_assn_raw_def by sepref
sepref_definition iv_is_empty_impl [llvm_inline] is "(RETURN o iv_is_empty)" :: "ivA⇧k →⇩a bool1_assn"
unfolding iv_is_empty_def iv_assn_raw_def by sepref
sepref_definition iv_inter_impl [llvm_inline] is "uncurry (RETURN oo iv_inter)" :: "ivA⇧k *⇩a ivA⇧k →⇩a ivA"
unfolding iv_inter_def iv_assn_raw_def max_def min_def by sepref
sepref_definition iv_card_impl [llvm_inline] is "RETURN o iv_card" :: "ivA⇧k →⇩a sA"
unfolding iv_card_def iv_assn_raw_def
apply (annot_snat_const "TYPE('l)")
by sepref
sepref_definition iv_range_lb_impl [llvm_inline] is "RETURN o id" :: "sA⇧k →⇩a sA"
by sepref
sepref_definition iv_inter_lb_impl [llvm_inline] is "uncurry (RETURN oo iv_inter_lb)" :: "sA⇧k *⇩a ivA⇧k →⇩a ivA"
unfolding iv_inter_lb_def iv_assn_raw_def max_def
by sepref
sepref_definition iv_split_card_impl [llvm_inline] is "uncurry (iv_split_card)" :: "sA⇧k *⇩a ivA⇧k →⇩a ivA ×⇩a ivA"
unfolding iv_split_card_def iv_assn_raw_def
by sepref
definition "iv_incr_elems_pre_aux ≡ λn (l,h) L. l<h ⟶ h+n < L"
sepref_definition iv_incr_elems_impl [llvm_inline] is "uncurry (RETURN oo iv_incr_elems)" :: "[λ(n,iv). iv_incr_elems_pre_aux n iv (max_snat L)]⇩a sA⇧k *⇩a ivA⇧k → ivA"
unfolding iv_incr_elems_def iv_assn_raw_def iv_incr_elems_pre_aux_def L_def
by sepref
text ‹Composing of Refinement Theorems›
definition "iv_assn ≡ hr_comp ivA iv_rel"
abbreviation "iv_assn' TYPE('l) ≡ iv_assn"
definition "iv_lb_assn ≡ hr_comp sA iv_lb_rel"
abbreviation "iv_lb_assn' TYPE('l) ≡ iv_lb_assn"
lemma iv_assn_pure[safe_constraint_rules,simp]: "is_pure iv_assn"
unfolding iv_assn_def iv_assn_raw_def
by solve_constraint
lemma iv_lb_assn_pure[safe_constraint_rules,simp]: "is_pure iv_lb_assn"
unfolding iv_lb_assn_def
by solve_constraint
lemmas [sepref_frame_free_rules] = mk_free_is_pure[OF iv_assn_pure] mk_free_is_pure[OF iv_lb_assn_pure]
lemma rdomp_iv_assn_strong: "rdomp iv_assn s ⟹ finite s ∧ iv_maxl s ≤ max_snat LENGTH('l)"
apply (auto
simp: iv_assn_def iv_assn_raw_def iv_rel_def in_br_conv iv_maxl_def iv_α_def
dest!: in_snat_rel_boundsD)
done
lemma rdomp_iv_assn[sepref_bounds_dest]: "rdomp iv_assn s ⟹ finite s"
by (auto simp: iv_assn_def iv_rel_def in_br_conv)
lemma iv_lb_assn_norm: "pure (snat_rel O iv_lb_rel) = iv_lb_assn"
unfolding iv_lb_assn_def
by (simp add: hr_comp_pure)
definition iv_incr_elems_pre :: "nat set ⇒ _" where "iv_incr_elems_pre s n N ≡ s≠{} ⟶ 1 + Max s + n < N"
lemma iv_incr_elems_norm_pre: "(iv,s)∈iv_rel ⟹ iv_incr_elems_pre_aux n iv N ⟷ iv_incr_elems_pre s n N"
unfolding iv_incr_elems_pre_def iv_incr_elems_pre_aux_def iv_maxl_def iv_rel_def iv_α_def
by (auto simp: in_br_conv)
context
notes [fcomp_norm_simps] = iv_assn_def[symmetric] iv_lb_assn_norm set_rel_id_simp
notes [fcomp_prenorm_simps] = iv_incr_elems_norm_pre
begin
sepref_decl_impl iv_range_impl.refine[FCOMP iv_range_refine] .
sepref_decl_impl iv_is_empty_impl.refine[FCOMP iv_is_empty_refine] uses op_set_is_empty.fref[of Id] .
sepref_decl_impl iv_inter_impl.refine[FCOMP iv_inter_refine] uses op_set_inter.fref[of Id, simplified id_set_constraint_simps] .
sepref_decl_impl iv_range_lb_impl.refine[FCOMP iv_lb_refine] .
sepref_decl_impl iv_inter_lb_impl.refine[FCOMP iv_inter_lb_refine] uses op_set_inter.fref[of Id, simplified id_set_constraint_simps] .
sepref_decl_impl iv_card_impl.refine[FCOMP iv_card_refine] uses op_set_card.fref[of Id, simplified id_set_constraint_simps] .
sepref_decl_impl iv_inter_impl.refine[FCOMP iv_inter_refine, THEN hfref_ttnd_commute_op, simplified is_comm_simps Inter_is_commutative] uses op_set_inter.fref[of Id, simplified id_set_constraint_simps] .
sepref_decl_impl iv_inter_lb_impl.refine[FCOMP iv_inter_lb_refine, THEN hfref_ttnd_commute_op, simplified is_comm_simps Inter_is_commutative] uses op_set_inter.fref[of Id, simplified id_set_constraint_simps] .
sepref_decl_impl iv_incr_elems_impl.refine[FCOMP iv_incr_elems_refine] by simp
lemmas [sepref_fr_rules] = iv_split_card_impl.refine[FCOMP iv_split_card_refine]
end
subsubsection ‹Interval Lists›
definition "ivl_assn_raw ≡ al_assn' TYPE('l::len2) iv_assn"
private abbreviation (input) "ivlA ≡ ivl_assn_raw"
sepref_definition ivl_empty_impl [llvm_inline] is "uncurry0 (RETURN ivl_empty)" :: "[λ_. 4<L]⇩a unit_assn⇧k → ivlA"
unfolding ivl_empty_def ivl_assn_raw_def al_fold_custom_empty[where 'l='l] L_def
by sepref
sepref_definition ivl_is_empty_impl [llvm_inline] is "RETURN o ivl_is_empty" :: "ivlA⇧k →⇩a bool1_assn"
unfolding ivl_is_empty_def ivl_assn_raw_def
by sepref
lemma rdomp_al_assn_iv_assn[sepref_bounds_dest]: "rdomp (al_assn' TYPE('l) iv_assn) ivl ⟹ length ivl < max_snat LENGTH('l) ∧ ivl_maxl ivl ≤ max_snat LENGTH('l) ∧ 4<LENGTH('l)"
apply (frule rdomp_al_assn_len_bound)
apply (drule rdomp_al_dest')
apply simp
by (metis (no_types, opaque_lifting) Suc_leI in_set_conv_nth ivl_max_bound_aux le_less_trans rdomp_iv_assn_strong zero_order(1))
sepref_definition ivl_add_impl [llvm_inline] is "uncurry ivl_add" :: "iv_assn⇧k *⇩a ivlA⇧d →⇩a ivlA"
unfolding ivl_add_def ivl_assn_raw_def
supply [sepref_bounds_dest] = rdomp_iv_assn_strong
by sepref
sepref_definition ivl_rm_subset_impl [llvm_inline] is "ivl_rm_subset" :: "ivlA⇧d →⇩a iv_assn ×⇩a ivlA"
unfolding ivl_rm_subset_def ivl_assn_raw_def by sepref
sepref_definition ivl_card_impl [llvm_code] is "ivl_card" :: "ivlA⇧k →⇩a sA"
unfolding ivl_card_def ivl_assn_raw_def
apply (rewrite nfoldli_by_idx)
apply (rewrite nfoldli_upt_by_while)
apply (annot_snat_const "TYPE('l)")
by sepref
definition "ivl_assn ≡ hr_comp ivlA ivl_rel"
abbreviation "ivl_assn' TYPE('l) ≡ ivl_assn"
lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure ivl_assn]
lemma ivl_assn_free[sepref_frame_free_rules]: "MK_FREE (ivl_assn) arl_free"
unfolding ivl_assn_def ivl_assn_raw_def by (rule sepref_frame_free_rules)+
lemma rdomp_ivl_assn[sepref_bounds_dest]: "rdomp (ivl_assn' TYPE('l::len2)) s ⟹ finite s ∧ 4<LENGTH('l)"
unfolding ivl_assn_def ivl_rel_def ivl_assn_raw_def
by (clarsimp simp: in_br_conv rdomp_al_assn_len_bound)
lemma iv_assn_comp_finite_eq: "hr_comp iv_assn (b_rel Id finite) = iv_assn"
apply (subst hr_comp_elim_b_rel)
apply (simp add: rdomp_iv_assn)
by simp
text ‹Composition of Refinement Lemmas›
context
notes [fcomp_norm_simps] = ivl_assn_def[symmetric] set_rel_id_simp iv_assn_comp_finite_eq
begin
thm ivl_empty_impl.refine[FCOMP ivl_empty_refine]
sepref_decl_impl (no_register) ivl_empty: ivl_empty_impl.refine[FCOMP ivl_empty_refine] uses op_set_empty.fref[where A=Id] by simp
sepref_decl_impl ivl_is_empty_impl.refine[FCOMP ivl_is_empty_refine] uses op_set_is_empty.fref[where A=Id] .
sepref_decl_impl (ismop) ivl_add_impl.refine[FCOMP ivl_add_refine] .
sepref_decl_impl (ismop) ivl_add_impl.refine[FCOMP ivl_add_refine, THEN hfref_ttnd_commute_op, simplified is_comm_simps Un_disj_is_commutative] .
sepref_decl_impl (ismop) ivl_card_impl.refine[FCOMP ivl_card_refine] uses mop_set_card.fref[of Id, simplified id_set_constraint_simps] .
lemmas [sepref_fr_rules] = ivl_rm_subset_impl.refine[FCOMP ivl_rm_subset_refine]
end
definition [simp]: "op_ivl_empty TYPE('l) = op_set_empty"
definition [simp]: "mop_ivl_empty TYPE('l) = mop_set_empty"
sepref_register
"op_ivl_empty TYPE('l)"
"mop_ivl_empty TYPE('l)"
lemma ivl_empty_fold_aux:
"op_set_empty = PR_CONST (op_ivl_empty TYPE('l))"
"mop_set_empty = PR_CONST (mop_ivl_empty TYPE('l))"
by auto
lemmas [sepref_fr_rules] =
ivl_empty_hnr[unfolded ivl_empty_fold_aux]
ivl_empty_hnr_mop[unfolded ivl_empty_fold_aux]
lemma ivl_fold_custom_empty:
"{} = op_ivl_empty TYPE('l)"
"op_set_empty = op_ivl_empty TYPE('l)"
"mop_set_empty = mop_ivl_empty TYPE('l)"
by auto
end
subsection ‹Directly Refined Set Operations›
definition "set_finite_inter s⇩1 s⇩2 ≡ doN {
ASSERT (finite s⇩2);
(r,s) ← WHILEIT (λ(r,s). r ∪ s⇩1∩s = s⇩1 ∩ s⇩2 ∧ r∩s={} ∧ finite s ) (λ(r,s). ¬op_set_is_empty s) (λ(r,s). doN {
(ss,s') ← mop_set_rm_subset s;
let ss = (ss∩s⇩1);
r ← mop_set_union_disj ss r;
RETURN (r,s')
}) ({},s⇩2);
RETURN r
}"
lemma set_finite_inter_refine: "(set_finite_inter, mop_set_inter) ∈ Id → b_rel Id finite → ⟨Id⟩nres_rel"
unfolding set_finite_inter_def
apply clarsimp
apply (refine_vcg WHILEIT_rule[where R="measure (card o snd)"])
apply (auto simp: card_Un_disjoint)
done
sepref_definition set_finite_inter_iv_ivl_impl [llvm_code] is "uncurry set_finite_inter"
:: "(iv_assn' TYPE('l::len2))⇧k *⇩a (ivl_assn' TYPE('l))⇧d →⇩a ivl_assn' TYPE('l)"
unfolding set_finite_inter_def
apply (simp only: ivl_fold_custom_empty[where 'l='l])
by sepref
sepref_definition set_finite_inter_lb_ivl_impl [llvm_code] is "uncurry set_finite_inter"
:: "(iv_lb_assn' TYPE('l::len2))⇧k *⇩a (ivl_assn' TYPE('l))⇧d →⇩a ivl_assn' TYPE('l)"
unfolding set_finite_inter_def
apply (simp only: ivl_fold_custom_empty[where 'l='l])
by sepref_dbg_keep
lemma ivl_assn_comp_finite_eq: "hr_comp ivl_assn (b_rel Id finite) = ivl_assn"
apply (subst hr_comp_elim_b_rel)
by (auto simp: ivl_assn_def ivl_rel_def in_br_conv)
context
notes [fcomp_norm_simps] = ivl_assn_comp_finite_eq set_rel_id_simp
begin
private lemmas iv_ivl_refine = set_finite_inter_iv_ivl_impl.refine[FCOMP set_finite_inter_refine]
private lemmas ivl_iv_refine = iv_ivl_refine[THEN hfref_ttnd_commute_op, simplified is_comm_simps Inter_is_commutative]
private lemmas lb_ivl_refine = set_finite_inter_lb_ivl_impl.refine[FCOMP set_finite_inter_refine]
private lemmas ivl_lb_refine = lb_ivl_refine[THEN hfref_ttnd_commute_op, simplified is_comm_simps Inter_is_commutative]
private lemmas mop_set_inter_id_fref = mop_set_inter.fref[of Id, simplified id_set_constraint_simps]
sepref_decl_impl (ismop) iv_ivl_refine uses mop_set_inter_id_fref .
sepref_decl_impl (ismop) ivl_iv_refine uses mop_set_inter_id_fref .
sepref_decl_impl (ismop) lb_ivl_refine uses mop_set_inter_id_fref .
sepref_decl_impl (ismop) ivl_lb_refine uses mop_set_inter_id_fref .
end
definition "set_finite_incr_elems (n::nat) s⇩0 ≡ doN {
ASSERT (finite s⇩0);
(r,s) ← WHILEIT (λ(r,s). (+)n`s⇩0 = r ∪ (+)n`s ∧ r ∩ (+)n`s = {} ∧ finite s ∧ s ⊆ s⇩0) (λ(r,s). ¬op_set_is_empty s) (λ(r,s). doN {
(ss,s') ← mop_set_rm_subset s;
ASSERT(ss ⊆ s⇩0);
let ss = op_set_incr_elems n ss;
r ← mop_set_union_disj ss r;
RETURN (r,s')
}) ({},s⇩0);
RETURN r
}"
lemma set_finite_incr_elems_refine: "(set_finite_incr_elems, mop_set_incr_elems) ∈ Id → b_rel Id finite → ⟨Id⟩nres_rel"
unfolding set_finite_incr_elems_def
apply clarsimp
apply (refine_vcg WHILEIT_rule[where R="measure (card o snd)"])
by (auto simp: card_Un_disjoint)
find_theorems "Max" "(⊆)"
lemma iv_incr_elems_pre_mono: "iv_incr_elems_pre s n N ⟹ finite s ⟹ s'⊆s ⟹ iv_incr_elems_pre s' n N" for n :: nat
unfolding iv_incr_elems_pre_def
by (auto dest: Max_mono)
definition "iv_incr_elems_abs_bound (s::nat set) n N ≡ s≠{} ⟶ Max s + n < N"
lemma iv_incr_elems_pre_from_abs_boundI[elim!]: "iv_incr_elems_abs_bound s n N ⟹ N<N' ⟹ iv_incr_elems_pre s n N'"
unfolding iv_incr_elems_abs_bound_def iv_incr_elems_pre_def by auto
lemma iv_incr_elems_abs_bound_card_boundI:
"s ⊆ {0..<N} ⟹ N+n≤N' ⟹ iv_incr_elems_abs_bound s n N'"
unfolding iv_incr_elems_abs_bound_def
apply clarsimp
apply (frule Max_mono)
by auto
lemma iv_incr_elems_abs_bound_card_boundI': "(+)n`s ⊆ {0..<N} ⟹ iv_incr_elems_abs_bound s n N"
unfolding iv_incr_elems_abs_bound_def
apply clarsimp
apply (subgoal_tac "n≤N" "s⊆{0..<N-n}")
apply (frule Max_mono[of s]; simp?)
by auto
lemma "s ⊆ {0..<N} ⟹ N+n<N' ⟹ iv_incr_elems_pre s n N'"
unfolding iv_incr_elems_pre_def
apply clarsimp
apply (frule Max_mono)
by auto
lemma "(+)n`s ⊆ {0..<N} ⟹ N<N' ⟹ iv_incr_elems_pre s n N'"
unfolding iv_incr_elems_pre_def
apply clarsimp
apply (subgoal_tac "n≤N" "s⊆{0..<N-n}")
apply (frule Max_mono[of s]; simp?)
by auto
context
fixes L
defines "L ≡ LENGTH('l::len2)"
begin
sepref_definition set_finite_incr_elems_ivl_impl [llvm_code] is "uncurry set_finite_incr_elems"
:: "[λ(n,s). iv_incr_elems_pre s n (max_snat L) ]⇩a (snat_assn' TYPE('l::len2))⇧k *⇩a (ivl_assn' TYPE('l))⇧d → ivl_assn' TYPE('l)"
unfolding set_finite_incr_elems_def L_def
apply (simp only: ivl_fold_custom_empty[where 'l='l])
supply [elim] = iv_incr_elems_pre_mono
by sepref
context
notes [fcomp_norm_simps] = ivl_assn_comp_finite_eq set_rel_id_simp
begin
sepref_decl_impl (ismop) set_finite_incr_elems_ivl_impl.refine[FCOMP set_finite_incr_elems_refine] by simp
end
end
end