Theory Gen_Set
section ‹\isaheader{Generic Set Algorithms}›
theory Gen_Set
imports "../Intf/Intf_Set" "../../Iterator/Iterator"
begin
lemma foldli_union: "det_fold_set X (λ_. True) insert a ((∪) a)"
proof (rule, goal_cases)
case (1 l) thus ?case
by (induct l arbitrary: a) auto
qed
definition gen_union
:: "_ ⇒ ('k ⇒ 's2 ⇒ 's2)
⇒ 's1 ⇒ 's2 ⇒ 's2"
where
"gen_union it ins A B ≡ it A (λ_. True) ins B"
lemma gen_union[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes INS: "GEN_OP ins Set.insert (Rk→⟨Rk⟩Rs2→⟨Rk⟩Rs2)"
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 tsl)"
shows "(gen_union (λx. foldli (tsl x)) ins,(∪))
∈ (⟨Rk⟩Rs1) → (⟨Rk⟩Rs2) → (⟨Rk⟩Rs2)"
apply (intro fun_relI)
apply (subst Un_commute)
unfolding gen_union_def
apply (rule det_fold_set[OF
foldli_union IT[unfolded autoref_tag_defs]])
using INS
unfolding autoref_tag_defs
apply (parametricity)+
done
lemma foldli_inter: "det_fold_set X (λ_. True)
(λx s. if x∈a then insert x s else s) {} (λs. s∩a)"
(is "det_fold_set _ _ ?f _ _")
proof -
{
fix l s0
have "foldli l (λ_. True)
(λx s. if x∈a then insert x s else s) s0 = s0 ∪ (set l ∩ a)"
by (induct l arbitrary: s0) auto
}
from this[of _ "{}"] show ?thesis apply - by rule simp
qed
definition gen_inter :: "_ ⇒
('k ⇒ 's2 ⇒ bool) ⇒ _"
where "gen_inter it1 memb2 ins3 empty3 s1 s2
≡ it1 s1 (λ_. True)
(λx s. if memb2 x s2 then ins3 x s else s) empty3"
lemma gen_inter[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 tsl)"
assumes MEMB:
"GEN_OP memb2 (∈) (Rk → ⟨Rk⟩Rs2 → Id)"
assumes INS:
"GEN_OP ins3 Set.insert (Rk→⟨Rk⟩Rs3→⟨Rk⟩Rs3)"
assumes EMPTY:
"GEN_OP empty3 {} (⟨Rk⟩Rs3)"
shows "(gen_inter (λx. foldli (tsl x)) memb2 ins3 empty3,(∩))
∈ (⟨Rk⟩Rs1) → (⟨Rk⟩Rs2) → (⟨Rk⟩Rs3)"
apply (intro fun_relI)
unfolding gen_inter_def
apply (rule det_fold_set[OF foldli_inter IT[unfolded autoref_tag_defs]])
using MEMB INS EMPTY
unfolding autoref_tag_defs
apply (parametricity)+
done
lemma foldli_diff:
"det_fold_set X (λ_. True) (λx s. op_set_delete x s) s ((-) s)"
proof (rule, goal_cases)
case (1 l) thus ?case
by (induct l arbitrary: s) auto
qed
definition gen_diff :: "('k⇒'s1⇒'s1) ⇒ _ ⇒ 's2 ⇒ _ "
where "gen_diff del1 it2 s1 s2
≡ it2 s2 (λ_. True) (λx s. del1 x s) s1"
lemma gen_diff[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes DEL:
"GEN_OP del1 op_set_delete (Rk → ⟨Rk⟩Rs1 → ⟨Rk⟩Rs1)"
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs2 it2)"
shows "(gen_diff del1 (λx. foldli (it2 x)),(-))
∈ (⟨Rk⟩Rs1) → (⟨Rk⟩Rs2) → (⟨Rk⟩Rs1)"
apply (intro fun_relI)
unfolding gen_diff_def
apply (rule det_fold_set[OF foldli_diff IT[unfolded autoref_tag_defs]])
using DEL
unfolding autoref_tag_defs
apply (parametricity)+
done
lemma foldli_ball_aux:
"foldli l (λx. x) (λx _. P x) b ⟷ b ∧ Ball (set l) P"
by (induct l arbitrary: b) auto
lemma foldli_ball: "det_fold_set X (λx. x) (λx _. P x) True (λs. Ball s P)"
apply rule using foldli_ball_aux[where b=True] by simp
definition gen_ball :: "_ ⇒ 's ⇒ ('k ⇒ bool) ⇒ _ "
where "gen_ball it s P ≡ it s (λx. x) (λx _. P x) True"
lemma gen_ball[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
shows "(gen_ball (λx. foldli (it x)),Ball) ∈ ⟨Rk⟩Rs → (Rk→Id) → Id"
apply (intro fun_relI)
unfolding gen_ball_def
apply (rule det_fold_set[OF foldli_ball IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done
lemma foldli_bex_aux: "foldli l (λx. ¬x) (λx _. P x) b ⟷ b ∨ Bex (set l) P"
by (induct l arbitrary: b) auto
lemma foldli_bex: "det_fold_set X (λx. ¬x) (λx _. P x) False (λs. Bex s P)"
apply rule using foldli_bex_aux[where b=False] by simp
definition gen_bex :: "_ ⇒ 's ⇒ ('k ⇒ bool) ⇒ _ "
where "gen_bex it s P ≡ it s (λx. ¬x) (λx _. P x) False"
lemma gen_bex[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
shows "(gen_bex (λx. foldli (it x)),Bex) ∈ ⟨Rk⟩Rs → (Rk→Id) → Id"
apply (intro fun_relI)
unfolding gen_bex_def
apply (rule det_fold_set[OF foldli_bex IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done
lemma ball_subseteq:
"(Ball s1 (λx. x∈s2)) ⟷ s1 ⊆ s2"
by blast
definition gen_subseteq
:: "('s1 ⇒ ('k ⇒ bool) ⇒ bool) ⇒ ('k ⇒ 's2 ⇒ bool) ⇒ _"
where "gen_subseteq ball1 mem2 s1 s2 ≡ ball1 s1 (λx. mem2 x s2)"
lemma gen_subseteq[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes "GEN_OP ball1 Ball (⟨Rk⟩Rs1 → (Rk→Id) → Id)"
assumes "GEN_OP mem2 (∈) (Rk → ⟨Rk⟩Rs2 → Id)"
shows "(gen_subseteq ball1 mem2,(⊆)) ∈ ⟨Rk⟩Rs1 → ⟨Rk⟩Rs2 → Id"
apply (intro fun_relI)
unfolding gen_subseteq_def using assms
unfolding autoref_tag_defs
apply -
apply (subst ball_subseteq[symmetric])
apply parametricity
done
definition "gen_equal ss1 ss2 s1 s2 ≡ ss1 s1 s2 ∧ ss2 s2 s1"
lemma gen_equal[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes "GEN_OP ss1 (⊆) (⟨Rk⟩Rs1 → ⟨Rk⟩Rs2 → Id)"
assumes "GEN_OP ss2 (⊆) (⟨Rk⟩Rs2 → ⟨Rk⟩Rs1 → Id)"
shows "(gen_equal ss1 ss2, (=)) ∈ ⟨Rk⟩Rs1 → ⟨Rk⟩Rs2 → Id"
apply (intro fun_relI)
unfolding gen_equal_def using assms
unfolding autoref_tag_defs
apply -
apply (subst set_eq_subset)
apply (parametricity)
done
lemma foldli_card_aux: "distinct l ⟹ foldli l (λ_. True)
(λ_ n. Suc n) n = n + card (set l)"
apply (induct l arbitrary: n)
apply auto
done
lemma foldli_card: "det_fold_set X (λ_. True) (λ_ n. Suc n) 0 card"
apply rule using foldli_card_aux[where n=0] by simp
definition gen_card where
"gen_card it s ≡ it s (λx. True) (λ_ n. Suc n) 0"
lemma gen_card[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
shows "(gen_card (λx. foldli (it x)),card) ∈ ⟨Rk⟩Rs → Id"
apply (intro fun_relI)
unfolding gen_card_def
apply (rule det_fold_set[OF foldli_card IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done
lemma fold_set: "fold Set.insert l s = s ∪ set l"
by (induct l arbitrary: s) auto
definition gen_set :: "'s ⇒ ('k ⇒ 's ⇒ 's) ⇒ _" where
"gen_set emp ins l = fold ins l emp"
lemma gen_set[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes EMPTY:
"GEN_OP emp {} (⟨Rk⟩Rs)"
assumes INS:
"GEN_OP ins Set.insert (Rk→⟨Rk⟩Rs→⟨Rk⟩Rs)"
shows "(gen_set emp ins,set)∈⟨Rk⟩list_rel→⟨Rk⟩Rs"
apply (intro fun_relI)
unfolding gen_set_def using assms
unfolding autoref_tag_defs
apply -
apply (subst fold_set[where s="{}",simplified,symmetric])
apply parametricity
done
lemma ball_isEmpty: "op_set_isEmpty s = (∀x∈s. False)"
by auto
definition gen_isEmpty :: "('s ⇒ ('k ⇒ bool) ⇒ bool) ⇒ 's ⇒ bool" where
"gen_isEmpty ball s ≡ ball s (λ_. False)"
lemma gen_isEmpty[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes "GEN_OP ball Ball (⟨Rk⟩Rs → (Rk→Id) → Id)"
shows "(gen_isEmpty ball,op_set_isEmpty) ∈ ⟨Rk⟩Rs → Id"
apply (intro fun_relI)
unfolding gen_isEmpty_def using assms
unfolding autoref_tag_defs
apply -
apply (subst ball_isEmpty)
apply parametricity
done
lemma foldli_size_abort_aux:
"⟦n0≤m; distinct l⟧ ⟹
foldli l (λn. n<m) (λ_ n. Suc n) n0 = min m (n0 + card (set l))"
apply (induct l arbitrary: n0)
apply auto
done
lemma foldli_size_abort: "
det_fold_set X (λn. n<m) (λ_ n. Suc n) 0 (op_set_size_abort m)"
apply rule
using foldli_size_abort_aux[where ?n0.0=0]
by simp
definition gen_size_abort where
"gen_size_abort it m s ≡ it s (λn. n<m) (λ_ n. Suc n) 0"
lemma gen_size_abort[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
shows "(gen_size_abort (λx. foldli (it x)),op_set_size_abort)
∈ Id → ⟨Rk⟩Rs → Id"
apply (intro fun_relI)
unfolding gen_size_abort_def
apply (rule det_fold_set[OF foldli_size_abort IT[unfolded autoref_tag_defs]])
apply (parametricity)+
done
lemma size_abort_isSng: "op_set_isSng s ⟷ op_set_size_abort 2 s = 1"
by auto
definition gen_isSng :: "(nat ⇒ 's ⇒ nat) ⇒ _" where
"gen_isSng sizea s ≡ sizea 2 s = 1"
lemma gen_isSng[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes "GEN_OP sizea op_set_size_abort (Id → (⟨Rk⟩Rs) → Id)"
shows "(gen_isSng sizea,op_set_isSng) ∈ ⟨Rk⟩Rs → Id"
apply (intro fun_relI)
unfolding gen_isSng_def using assms
unfolding autoref_tag_defs
apply -
apply (subst size_abort_isSng)
apply parametricity
done
lemma foldli_disjoint_aux:
"foldli l1 (λx. x) (λx _. ¬x∈s2) b ⟷ b ∧ op_set_disjoint (set l1) s2"
by (induct l1 arbitrary: b) auto
lemma foldli_disjoint:
"det_fold_set X (λx. x) (λx _. ¬x∈s2) True (λs1. op_set_disjoint s1 s2)"
apply rule using foldli_disjoint_aux[where b=True] by simp
definition gen_disjoint
:: "_ ⇒ ('k⇒'s2⇒bool) ⇒ _"
where "gen_disjoint it1 mem2 s1 s2
≡ it1 s1 (λx. x) (λx _. ¬mem2 x s2) True"
lemma gen_disjoint[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
assumes MEM: "GEN_OP mem2 (∈) (Rk → ⟨Rk⟩Rs2 → Id)"
shows "(gen_disjoint (λx. foldli (it1 x)) mem2,op_set_disjoint)
∈ ⟨Rk⟩Rs1 → ⟨Rk⟩Rs2 → Id"
apply (intro fun_relI)
unfolding gen_disjoint_def
apply (rule det_fold_set[OF foldli_disjoint IT[unfolded autoref_tag_defs]])
using MEM unfolding autoref_tag_defs
apply (parametricity)+
done
lemma foldli_filter_aux:
"foldli l (λ_. True) (λx s. if P x then insert x s else s) s0
= s0 ∪ op_set_filter P (set l)"
by (induct l arbitrary: s0) auto
lemma foldli_filter:
"det_fold_set X (λ_. True) (λx s. if P x then insert x s else s) {}
(op_set_filter P)"
apply rule using foldli_filter_aux[where ?s0.0="{}"] by simp
definition gen_filter
where "gen_filter it1 emp2 ins2 P s1 ≡
it1 s1 (λ_. True) (λx s. if P x then ins2 x s else s) emp2"
lemma gen_filter[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
assumes INS:
"GEN_OP ins2 Set.insert (Rk→⟨Rk⟩Rs2→⟨Rk⟩Rs2)"
assumes EMPTY:
"GEN_OP empty2 {} (⟨Rk⟩Rs2)"
shows "(gen_filter (λx. foldli (it1 x)) empty2 ins2,op_set_filter)
∈ (Rk→Id) → (⟨Rk⟩Rs1) → (⟨Rk⟩Rs2)"
apply (intro fun_relI)
unfolding gen_filter_def
apply (rule det_fold_set[OF foldli_filter IT[unfolded autoref_tag_defs]])
using INS EMPTY unfolding autoref_tag_defs
apply (parametricity)+
done
lemma foldli_image_aux:
"foldli l (λ_. True) (λx s. insert (f x) s) s0
= s0 ∪ f`(set l)"
by (induct l arbitrary: s0) auto
lemma foldli_image:
"det_fold_set X (λ_. True) (λx s. insert (f x) s) {}
((`) f)"
apply rule using foldli_image_aux[where ?s0.0="{}"] by simp
definition gen_image
where "gen_image it1 emp2 ins2 f s1 ≡
it1 s1 (λ_. True) (λx s. ins2 (f x) s) emp2"
lemma gen_image[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
assumes INS:
"GEN_OP ins2 Set.insert (Rk'→⟨Rk'⟩Rs2→⟨Rk'⟩Rs2)"
assumes EMPTY:
"GEN_OP empty2 {} (⟨Rk'⟩Rs2)"
shows "(gen_image (λx. foldli (it1 x)) empty2 ins2,(`))
∈ (Rk→Rk') → (⟨Rk⟩Rs1) → (⟨Rk'⟩Rs2)"
apply (intro fun_relI)
unfolding gen_image_def
apply (rule det_fold_set[OF foldli_image IT[unfolded autoref_tag_defs]])
using INS EMPTY unfolding autoref_tag_defs
apply (parametricity)+
done
lemma foldli_pick:
assumes "l≠[]"
obtains x where "x∈set l"
and "(foldli l (case_option True (λ_. False)) (λx _. Some x) None) = Some x"
using assms by (cases l) auto
definition gen_pick where
"gen_pick it s ≡
(the (it s (case_option True (λ_. False)) (λx _. Some x) None))"
context begin interpretation autoref_syn .
lemma gen_pick[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT: "SIDE_GEN_ALGO (is_set_to_list Rk Rs it)"
assumes NE: "SIDE_PRECOND (s'≠{})"
assumes SREF: "(s,s')∈⟨Rk⟩Rs"
shows "(RETURN (gen_pick (λx. foldli (it x)) s),
(OP op_set_pick ::: ⟨Rk⟩Rs→⟨Rk⟩nres_rel)$s')∈⟨Rk⟩nres_rel"
proof -
obtain tsl' where
[param]: "(it s,tsl') ∈ ⟨Rk⟩list_rel"
and IT': "RETURN tsl' ≤ it_to_sorted_list (λ_ _. True) s'"
using IT[unfolded autoref_tag_defs is_set_to_list_def] SREF
by (rule is_set_to_sorted_listE)
from IT' NE have "tsl'≠[]" and [simp]: "s'=set tsl'"
unfolding it_to_sorted_list_def by simp_all
then obtain x where "x∈s'" and
"(foldli tsl' (case_option True (λ_. False)) (λx _. Some x) None) = Some x"
(is "?fld = _")
by (blast elim: foldli_pick)
moreover
have "(RETURN (gen_pick (λx. foldli (it x)) s), RETURN (the ?fld))
∈ ⟨Rk⟩nres_rel"
unfolding gen_pick_def
apply (parametricity add: the_paramR)
using ‹?fld = Some x›
by simp
ultimately show ?thesis
unfolding autoref_tag_defs
apply -
apply (drule nres_relD)
apply (rule nres_relI)
apply (erule ref_two_step)
by simp
qed
end
definition gen_Sigma
where "gen_Sigma it1 it2 empX insX s1 f2 ≡
it1 s1 (λ_. True) (λx s.
it2 (f2 x) (λ_. True) (λy s. insX (x,y) s) s
) empX
"
lemma foldli_Sigma_aux:
fixes s :: "'s1_impl" and s':: "'k set"
fixes f :: "'k_impl ⇒ 's2_impl" and f':: "'k ⇒ 'l set"
fixes s0 :: "'kl_impl" and s0' :: "('k×'l) set"
assumes IT1: "is_set_to_list Rk Rs1 it1"
assumes IT2: "is_set_to_list Rl Rs2 it2"
assumes INS:
"(insX, Set.insert) ∈
(⟨Rk,Rl⟩prod_rel→⟨⟨Rk,Rl⟩prod_rel⟩Rs3→⟨⟨Rk,Rl⟩prod_rel⟩Rs3)"
assumes S0R: "(s0, s0') ∈ ⟨⟨Rk,Rl⟩prod_rel⟩Rs3"
assumes SR: "(s, s') ∈ ⟨Rk⟩Rs1"
assumes FR: "(f, f') ∈ Rk → ⟨Rl⟩Rs2"
shows "(foldli (it1 s) (λ_. True) (λx s.
foldli (it2 (f x)) (λ_. True) (λy s. insX (x,y) s) s
) s0,s0' ∪ Sigma s' f')
∈ ⟨⟨Rk,Rl⟩prod_rel⟩Rs3"
proof -
have S: "⋀x s f. Sigma (insert x s) f = ({x}×f x) ∪ Sigma s f"
by auto
obtain l' where
IT1L: "(it1 s,l')∈⟨Rk⟩list_rel"
and SL: "s' = set l'"
apply (rule
is_set_to_sorted_listE[OF IT1[unfolded is_set_to_list_def] SR])
by (auto simp: it_to_sorted_list_def)
show ?thesis
unfolding SL
using IT1L S0R
proof (induct arbitrary: s0 s0' rule: list_rel_induct)
case Nil thus ?case by simp
next
case (Cons x x' l l')
obtain l2' where
IT2L: "(it2 (f x),l2')∈⟨Rl⟩list_rel"
and FXL: "f' x' = set l2'"
apply (rule
is_set_to_sorted_listE[
OF IT2[unfolded is_set_to_list_def], of "f x" "f' x'"
])
apply (parametricity add: Cons.hyps(1) FR)
by (auto simp: it_to_sorted_list_def)
have "(foldli (it2 (f x)) (λ_. True) (λy. insX (x, y)) s0,
s0' ∪ {x'}×f' x') ∈ ⟨⟨Rk,Rl⟩prod_rel⟩Rs3"
unfolding FXL
using IT2L ‹(s0, s0') ∈ ⟨⟨Rk, Rl⟩prod_rel⟩Rs3›
apply (induct arbitrary: s0 s0' rule: list_rel_induct)
apply simp
apply simp
apply (subst Un_insert_left[symmetric])
apply (rprems)
apply (parametricity add: INS ‹(x,x')∈Rk›)
done
show ?case
apply simp
apply (subst S)
apply (subst Un_assoc[symmetric])
apply (rule Cons.hyps)
apply fact
done
qed
qed
lemma gen_Sigma[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes IT1: "SIDE_GEN_ALGO (is_set_to_list Rk Rs1 it1)"
assumes IT2: "SIDE_GEN_ALGO (is_set_to_list Rl Rs2 it2)"
assumes EMPTY:
"GEN_OP empX {} (⟨⟨Rk,Rl⟩prod_rel⟩Rs3)"
assumes INS:
"GEN_OP insX Set.insert
(⟨Rk,Rl⟩prod_rel→⟨⟨Rk,Rl⟩prod_rel⟩Rs3→⟨⟨Rk,Rl⟩prod_rel⟩Rs3)"
shows "(gen_Sigma (λx. foldli (it1 x)) (λx. foldli (it2 x)) empX insX,Sigma)
∈ (⟨Rk⟩Rs1) → (Rk → ⟨Rl⟩Rs2) → ⟨⟨Rk,Rl⟩prod_rel⟩Rs3"
apply (intro fun_relI)
unfolding gen_Sigma_def
using foldli_Sigma_aux[OF
IT1[unfolded autoref_tag_defs]
IT2[unfolded autoref_tag_defs]
INS[unfolded autoref_tag_defs]
EMPTY[unfolded autoref_tag_defs]
]
by simp
lemma gen_cart:
assumes PRIO_TAG_GEN_ALGO
assumes [param]: "(sigma, Sigma) ∈ (⟨Rx⟩Rsx → (Rx → ⟨Ry⟩Rsy) → ⟨Rx ×⇩r Ry⟩Rsp)"
shows "(λx y. sigma x (λ_. y), op_set_cart) ∈ ⟨Rx⟩Rsx → ⟨Ry⟩Rsy → ⟨Rx ×⇩r Ry⟩Rsp"
unfolding op_set_cart_def[abs_def]
by parametricity
lemmas [autoref_rules] = gen_cart[OF _ GEN_OP_D]
context begin interpretation autoref_syn .
lemma op_set_to_sorted_list_autoref[autoref_rules]:
assumes "SIDE_GEN_ALGO (is_set_to_sorted_list ordR Rk Rs tsl)"
shows "(λsi. RETURN (tsl si), OP (op_set_to_sorted_list ordR))
∈ ⟨Rk⟩Rs → ⟨⟨Rk⟩list_rel⟩nres_rel"
using assms
apply (intro fun_relI nres_relI)
apply simp
apply (rule RETURN_SPEC_refine)
apply (auto simp: is_set_to_sorted_list_def it_to_sorted_list_def)
done
lemma op_set_to_list_autoref[autoref_rules]:
assumes "SIDE_GEN_ALGO (is_set_to_sorted_list ordR Rk Rs tsl)"
shows "(λsi. RETURN (tsl si), op_set_to_list)
∈ ⟨Rk⟩Rs → ⟨⟨Rk⟩list_rel⟩nres_rel"
using assms
apply (intro fun_relI nres_relI)
apply simp
apply (rule RETURN_SPEC_refine)
apply (auto simp: is_set_to_sorted_list_def it_to_sorted_list_def)
done
end
lemma foldli_Union: "det_fold_set X (λ_. True) (∪) {} Union"
proof (rule, goal_cases)
case (1 l)
have "∀a. foldli l (λ_. True) (∪) a = a ∪ ⋃(set l)"
by (induct l) auto
thus ?case by auto
qed
definition gen_Union
:: "_ ⇒ 's3 ⇒ ('s2 ⇒ 's3 ⇒ 's3)
⇒ 's1 ⇒ 's3"
where
"gen_Union it emp un X ≡ it X (λ_. True) un emp"
lemma gen_Union[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes EMP: "GEN_OP emp {} (⟨Rk⟩Rs3)"
assumes UN: "GEN_OP un (∪) (⟨Rk⟩Rs2→⟨Rk⟩Rs3→⟨Rk⟩Rs3)"
assumes IT: "SIDE_GEN_ALGO (is_set_to_list (⟨Rk⟩Rs2) Rs1 tsl)"
shows "(gen_Union (λx. foldli (tsl x)) emp un,Union) ∈ ⟨⟨Rk⟩Rs2⟩Rs1 → ⟨Rk⟩Rs3"
apply (intro fun_relI)
unfolding gen_Union_def
apply (rule det_fold_set[OF
foldli_Union IT[unfolded autoref_tag_defs]])
using EMP UN
unfolding autoref_tag_defs
apply (parametricity)+
done
definition "atLeastLessThan_impl a b ≡ do {
(_,r) ← WHILET (λ(i,r). i<b) (λ(i,r). RETURN (i+1, insert i r)) (a,{});
RETURN r
}"
lemma atLeastLessThan_impl_correct:
"atLeastLessThan_impl a b ≤ SPEC (λr. r = {a..<b::nat})"
unfolding atLeastLessThan_impl_def
apply (refine_rcg refine_vcg WHILET_rule[where
I = "λ(i,r). r = {a..<i} ∧ a≤i ∧ ((a<b ⟶ i≤b) ∧ (¬a<b ⟶ i=a))"
and R = "measure (λ(i,_). b - i)"
])
by auto
schematic_goal atLeastLessThan_code_aux:
notes [autoref_rules] = IdI[of a] IdI[of b]
assumes [autoref_rules]: "(emp,{})∈Rs"
assumes [autoref_rules]: "(ins,insert)∈nat_rel → Rs → Rs"
shows "(?c, atLeastLessThan_impl)
∈ nat_rel → nat_rel → ⟨Rs⟩nres_rel"
unfolding atLeastLessThan_impl_def[abs_def]
apply (autoref (keep_goal))
done
concrete_definition atLeastLessThan_code uses atLeastLessThan_code_aux
schematic_goal atLeastLessThan_tr_aux:
"RETURN ?c ≤ atLeastLessThan_code emp ins a b"
unfolding atLeastLessThan_code_def
by (refine_transfer (post))
concrete_definition atLeastLessThan_tr
for emp ins a b uses atLeastLessThan_tr_aux
lemma atLeastLessThan_gen[autoref_rules]:
assumes "PRIO_TAG_GEN_ALGO"
assumes "GEN_OP emp {} Rs"
assumes "GEN_OP ins insert (nat_rel → Rs → Rs)"
shows "(atLeastLessThan_tr emp ins, atLeastLessThan)
∈ nat_rel → nat_rel → Rs"
proof (intro fun_relI, simp)
fix a b
from assms have GEN:
"(emp,{})∈Rs" "(ins,insert)∈nat_rel → Rs → Rs"
by auto
note atLeastLessThan_tr.refine[of emp ins a b]
also note
atLeastLessThan_code.refine[OF GEN,param_fo, OF IdI IdI, THEN nres_relD]
also note atLeastLessThan_impl_correct
finally show "(atLeastLessThan_tr emp ins a b, {a..<b}) ∈ Rs"
by (auto simp: pw_le_iff refine_pw_simps)
qed
end