Theory Gen_Iterator
section ‹\isaheader{Iterators}›
theory Gen_Iterator
imports Refine_Monadic.Refine_Monadic Proper_Iterator
begin
text ‹
Iterators are realized by to-list functions followed by folding.
A post-optimization step then replaces these constructions by
real iterators.›
lemma param_it_to_list[param]: "(it_to_list,it_to_list) ∈
(Rs → (Ra → bool_rel) →
(Rb → ⟨Rb⟩list_rel → ⟨Rb⟩list_rel) → ⟨Rc⟩list_rel → Rd) → Rs → Rd"
unfolding it_to_list_def[abs_def]
by parametricity
definition key_rel :: "('k ⇒ 'k ⇒ bool) ⇒ ('k×'v) ⇒ ('k×'v) ⇒ bool"
where "key_rel R a b ≡ R (fst a) (fst b)"
lemma key_rel_UNIV[simp]: "key_rel (λ_ _. True) = (λ_ _. True)"
unfolding key_rel_def[abs_def] by auto
subsection ‹Setup for Autoref›
text ‹Default pattern rules for ‹it_to_sorted_list››
definition "set_to_sorted_list R S ≡ it_to_sorted_list R S"
lemma set_to_sorted_list_itype[autoref_itype]:
"set_to_sorted_list R ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨⟨I⟩⇩ii_list⟩⇩ii_nres"
by simp
context begin interpretation autoref_syn .
lemma set_to_sorted_list_pat[autoref_op_pat]:
"it_to_sorted_list R S ≡ OP (set_to_sorted_list R) S"
unfolding set_to_sorted_list_def[abs_def] by auto
end
definition "map_to_sorted_list R M
≡ it_to_sorted_list (key_rel R) (map_to_set M)"
lemma map_to_sorted_list_itype[autoref_itype]:
"map_to_sorted_list R ::⇩i ⟨Rk,Rv⟩⇩ii_map →⇩i ⟨⟨⟨Rk,Rv⟩⇩ii_prod⟩⇩ii_list⟩⇩ii_nres"
by simp
context begin interpretation autoref_syn .
lemma map_to_sorted_list_pat[autoref_op_pat]:
"it_to_sorted_list (key_rel R) (map_to_set M)
≡ OP (map_to_sorted_list R) M"
"it_to_sorted_list (λ_ _. True) (map_to_set M)
≡ OP (map_to_sorted_list (λ_ _. True)) M"
unfolding map_to_sorted_list_def[abs_def] by auto
end
subsection ‹Set iterators›
definition "is_set_to_sorted_list ordR Rk Rs tsl ≡ ∀s s'.
(s,s')∈⟨Rk⟩Rs
⟶ ( ∃l'. (tsl s,l')∈⟨Rk⟩list_rel
∧ RETURN l' ≤ it_to_sorted_list ordR s')"
definition "is_set_to_list ≡ is_set_to_sorted_list (λ_ _. True)"
lemma is_set_to_sorted_listE:
assumes "is_set_to_sorted_list ordR Rk Rs tsl"
assumes "(s,s')∈⟨Rk⟩Rs"
obtains l' where "(tsl s,l')∈⟨Rk⟩list_rel"
and "RETURN l' ≤ it_to_sorted_list ordR s'"
using assms unfolding is_set_to_sorted_list_def by blast
lemma it_to_sorted_list_weaken:
"R≤R' ⟹ it_to_sorted_list R s ≤ it_to_sorted_list R' s"
unfolding it_to_sorted_list_def
by (auto intro!: sorted_wrt_mono_rel[where P=R])
lemma set_to_list_by_set_to_sorted_list[autoref_ga_rules]:
assumes "GEN_ALGO_tag (is_set_to_sorted_list ordR Rk Rs tsl)"
shows "is_set_to_list Rk Rs tsl"
using assms
unfolding is_set_to_list_def is_set_to_sorted_list_def autoref_tag_defs
apply (safe)
apply (drule spec, drule spec, drule (1) mp)
apply (elim exE conjE)
apply (rule exI, rule conjI, assumption)
apply (rule order_trans, assumption)
apply (rule it_to_sorted_list_weaken)
by blast
definition "det_fold_set R c f σ result ≡
∀l. distinct l ∧ sorted_wrt R l ⟶ foldli l c f σ = result (set l)"
lemma det_fold_setI[intro?]:
assumes "⋀l. ⟦distinct l; sorted_wrt R l⟧
⟹ foldli l c f σ = result (set l)"
shows "det_fold_set R c f σ result"
using assms unfolding det_fold_set_def by auto
text ‹Template lemma for generic algorithm using set iterator›
lemma det_fold_sorted_set:
assumes 1: "det_fold_set ordR c' f' σ' result"
assumes 2: "is_set_to_sorted_list ordR Rk Rs tsl"
assumes SREF[param]: "(s,s')∈⟨Rk⟩Rs"
assumes [param]: "(c,c')∈Rσ→Id"
assumes [param]: "(f,f')∈Rk → Rσ → Rσ"
assumes [param]: "(σ,σ')∈Rσ"
shows "(foldli (tsl s) c f σ, result s') ∈ Rσ"
proof -
obtain tsl' where
[param]: "(tsl s,tsl') ∈ ⟨Rk⟩list_rel"
and IT: "RETURN tsl' ≤ it_to_sorted_list ordR s'"
using 2 SREF
by (rule is_set_to_sorted_listE)
have "(foldli (tsl s) c f σ, foldli tsl' c' f' σ') ∈ Rσ"
by parametricity
also have "foldli tsl' c' f' σ' = result s'"
using 1 IT
unfolding det_fold_set_def it_to_sorted_list_def
by simp
finally show ?thesis .
qed
lemma det_fold_set:
assumes "det_fold_set (λ_ _. True) c' f' σ' result"
assumes "is_set_to_list Rk Rs tsl"
assumes "(s,s')∈⟨Rk⟩Rs"
assumes "(c,c')∈Rσ→Id"
assumes "(f,f')∈Rk → Rσ → Rσ"
assumes "(σ,σ')∈Rσ"
shows "(foldli (tsl s) c f σ, result s') ∈ Rσ"
using assms
unfolding is_set_to_list_def
by (rule det_fold_sorted_set)
subsection ‹Map iterators›
text ‹Build relation on keys›
definition "is_map_to_sorted_list ordR Rk Rv Rm tsl ≡ ∀m m'.
(m,m')∈⟨Rk,Rv⟩Rm ⟶ (
∃l'. (tsl m,l')∈⟨⟨Rk,Rv⟩prod_rel⟩list_rel
∧ RETURN l' ≤ it_to_sorted_list (key_rel ordR) (map_to_set m'))"
definition "is_map_to_list Rk Rv Rm tsl
≡ is_map_to_sorted_list (λ_ _. True) Rk Rv Rm tsl"
lemma is_map_to_sorted_listE:
assumes "is_map_to_sorted_list ordR Rk Rv Rm tsl"
assumes "(m,m')∈⟨Rk,Rv⟩Rm"
obtains l' where "(tsl m,l')∈⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
and "RETURN l' ≤ it_to_sorted_list (key_rel ordR) (map_to_set m')"
using assms unfolding is_map_to_sorted_list_def by blast
lemma map_to_list_by_map_to_sorted_list[autoref_ga_rules]:
assumes "GEN_ALGO_tag (is_map_to_sorted_list ordR Rk Rv Rm tsl)"
shows "is_map_to_list Rk Rv Rm tsl"
using assms
unfolding is_map_to_list_def is_map_to_sorted_list_def autoref_tag_defs
apply (safe)
apply (drule spec, drule spec, drule (1) mp)
apply (elim exE conjE)
apply (rule exI, rule conjI, assumption)
apply (rule order_trans, assumption)
apply (rule it_to_sorted_list_weaken)
unfolding key_rel_def[abs_def]
by blast
definition "det_fold_map R c f σ result ≡
∀l. distinct (map fst l) ∧ sorted_wrt (key_rel R) l
⟶ foldli l c f σ = result (map_of l)"
lemma det_fold_mapI[intro?]:
assumes "⋀l. ⟦distinct (map fst l); sorted_wrt (key_rel R) l⟧
⟹ foldli l c f σ = result (map_of l)"
shows "det_fold_map R c f σ result"
using assms unfolding det_fold_map_def by auto
lemma det_fold_map_aux:
assumes 1: "⟦distinct (map fst l); sorted_wrt (key_rel R) l ⟧
⟹ foldli l c f σ = result (map_of l)"
assumes 2: "RETURN l ≤ it_to_sorted_list (key_rel R) (map_to_set m)"
shows "foldli l c f σ = result m"
proof -
from 2 have "distinct l" and "set l = map_to_set m"
and SORTED: "sorted_wrt (key_rel R) l"
unfolding it_to_sorted_list_def by simp_all
hence "∀(k,v)∈set l. ∀(k',v')∈set l. k=k' ⟶ v=v'"
apply simp
unfolding map_to_set_def
apply auto
done
with ‹distinct l› have DF: "distinct (map fst l)"
apply (induct l)
apply simp
apply force
done
with ‹set l = map_to_set m› have [simp]: "m = map_of l"
by (metis map_of_map_to_set)
from 1[OF DF SORTED] show ?thesis by simp
qed
text ‹Template lemma for generic algorithm using map iterator›
lemma det_fold_sorted_map:
assumes 1: "det_fold_map ordR c' f' σ' result"
assumes 2: "is_map_to_sorted_list ordR Rk Rv Rm tsl"
assumes MREF[param]: "(m,m')∈⟨Rk,Rv⟩Rm"
assumes [param]: "(c,c')∈Rσ→Id"
assumes [param]: "(f,f')∈⟨Rk,Rv⟩prod_rel → Rσ → Rσ"
assumes [param]: "(σ,σ')∈Rσ"
shows "(foldli (tsl m) c f σ, result m') ∈ Rσ"
proof -
obtain tsl' where
[param]: "(tsl m,tsl') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
and IT: "RETURN tsl' ≤ it_to_sorted_list (key_rel ordR) (map_to_set m')"
using 2 MREF by (rule is_map_to_sorted_listE)
have "(foldli (tsl m) c f σ, foldli tsl' c' f' σ') ∈ Rσ"
by parametricity
also have "foldli tsl' c' f' σ' = result m'"
using det_fold_map_aux[of tsl' ordR c' f' σ' result] 1 IT
unfolding det_fold_map_def
by clarsimp
finally show ?thesis .
qed
lemma det_fold_map:
assumes "det_fold_map (λ_ _. True) c' f' σ' result"
assumes "is_map_to_list Rk Rv Rm tsl"
assumes "(m,m')∈⟨Rk,Rv⟩Rm"
assumes "(c,c')∈Rσ→Id"
assumes "(f,f')∈⟨Rk,Rv⟩prod_rel → Rσ → Rσ"
assumes "(σ,σ')∈Rσ"
shows "(foldli (tsl m) c f σ, result m') ∈ Rσ"
using assms
unfolding is_map_to_list_def
by (rule det_fold_sorted_map)
lemma set_to_sorted_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 11)"
assumes TSL: "SIDE_GEN_ALGO (is_set_to_sorted_list R Rk Rs tsl)"
shows "(λs. RETURN (tsl s), set_to_sorted_list R)
∈ ⟨Rk⟩Rs → ⟨⟨Rk⟩list_rel⟩nres_rel"
proof (intro fun_relI nres_relI)
fix s s'
assume "(s,s')∈⟨Rk⟩Rs"
with TSL obtain l' where
R1: "(tsl s, l') ∈ ⟨Rk⟩list_rel"
and R2: "RETURN l' ≤ set_to_sorted_list R s'"
unfolding is_set_to_sorted_list_def set_to_sorted_list_def autoref_tag_defs
by blast
have "RETURN (tsl s) ≤ ⇓(⟨Rk⟩list_rel) (RETURN l')"
by (rule RETURN_refine) fact
also note R2
finally show "RETURN (tsl s) ≤ ⇓ (⟨Rk⟩list_rel) (set_to_sorted_list R s')" .
qed
lemma set_to_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 10)"
assumes TSL: "SIDE_GEN_ALGO (is_set_to_list Rk Rs tsl)"
shows "(λs. RETURN (tsl s), set_to_sorted_list (λ_ _. True))
∈ ⟨Rk⟩Rs → ⟨⟨Rk⟩list_rel⟩nres_rel"
using assms(2-) unfolding is_set_to_list_def
by (rule set_to_sorted_list_by_tsl[OF PRIO_TAGI])
lemma map_to_sorted_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 11)"
assumes TSL: "SIDE_GEN_ALGO (is_map_to_sorted_list R Rk Rv Rs tsl)"
shows "(λs. RETURN (tsl s), map_to_sorted_list R)
∈ ⟨Rk,Rv⟩Rs → ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩nres_rel"
proof (intro fun_relI nres_relI)
fix s s'
assume "(s,s')∈⟨Rk,Rv⟩Rs"
with TSL obtain l' where
R1: "(tsl s, l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
and R2: "RETURN l' ≤ map_to_sorted_list R s'"
unfolding is_map_to_sorted_list_def map_to_sorted_list_def autoref_tag_defs
by blast
have "RETURN (tsl s) ≤ ⇓(⟨⟨Rk,Rv⟩prod_rel⟩list_rel) (RETURN l')"
apply (rule RETURN_refine)
by fact
also note R2
finally show
"RETURN (tsl s) ≤ ⇓ (⟨⟨Rk,Rv⟩prod_rel⟩list_rel) (map_to_sorted_list R s')" .
qed
lemma map_to_list_by_tsl[autoref_rules]:
assumes "MINOR_PRIO_TAG (- 10)"
assumes TSL: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs tsl)"
shows "(λs. RETURN (tsl s), map_to_sorted_list (λ_ _. True))
∈ ⟨Rk,Rv⟩Rs → ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩nres_rel"
using assms(2-) unfolding is_map_to_list_def
by (rule map_to_sorted_list_by_tsl[OF PRIO_TAGI])
text ‹
TODO/FIXME:
* Integrate mono-prover properly into solver-infrastructure,
i.e. tag a mono-goal.
* Tag iterators, such that, for the mono-prover, we can just convert
a proper iterator back to its foldli-equivalent!
›
lemma proper_it_mono_dres_pair:
assumes PR: "proper_it' it it'"
assumes A: "⋀k v x. f k v x ≤ f' k v x"
shows "
it' s (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ
≤ it' s (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ" (is "?a ≤ ?b")
proof -
from proper_itE[OF PR[THEN proper_it'D]] obtain l where
A_FMT:
"?a = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ"
(is "_ = ?a'")
and B_FMT:
"?b = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ"
(is "_ = ?b'")
by metis
from A have A': "⋀kv x. case_prod f kv x ≤ case_prod f' kv x"
by auto
note A_FMT
also have
"?a' = foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f kv) σ"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note foldli_mono_dres[OF A']
also have
"foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f' kv) σ = ?b'"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note B_FMT[symmetric]
finally show ?thesis .
qed
lemma proper_it_mono_dres_pair_flat:
assumes PR: "proper_it' it it'"
assumes A: "⋀k v x. flat_ge (f k v x) (f' k v x)"
shows "
flat_ge (it' s (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ)
(it' s (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ)"
(is "flat_ge ?a ?b")
proof -
from proper_itE[OF PR[THEN proper_it'D]] obtain l where
A_FMT:
"?a = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f k v) σ"
(is "_ = ?a'")
and B_FMT:
"?b = foldli l (case_dres False False c) (λ(k,v) s. s ⤜ f' k v) σ"
(is "_ = ?b'")
by metis
from A have A': "⋀kv x. flat_ge (case_prod f kv x) (case_prod f' kv x)"
by auto
note A_FMT
also have
"?a' = foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f kv) σ"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note foldli_mono_dres_flat[OF A']
also have
"foldli l (case_dres False False c) (λkv s. s ⤜ case_prod f' kv) σ = ?b'"
apply (fo_rule fun_cong)
apply (fo_rule arg_cong)
by auto
also note B_FMT[symmetric]
finally show ?thesis .
qed
lemma proper_it_mono_dres:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. f kv x ≤ f' kv x"
shows "
it' s (case_dres False False c) (λkv s. s ⤜ f kv) σ
≤ it' s (case_dres False False c) (λkv s. s ⤜ f' kv) σ"
apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
apply (erule_tac t="it' s" in ssubst)
apply (rule foldli_mono_dres[OF A])
done
lemma proper_it_mono_dres_flat:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. flat_ge (f kv x) (f' kv x)"
shows "
flat_ge (it' s (case_dres False False c) (λkv s. s ⤜ f kv) σ)
(it' s (case_dres False False c) (λkv s. s ⤜ f' kv) σ)"
apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
apply (erule_tac t="it' s" in ssubst)
apply (rule foldli_mono_dres_flat[OF A])
done
lemma pi'_dom[icf_proper_iteratorI]: "proper_it' it it'
⟹ proper_it' (map_iterator_dom o it) (map_iterator_dom o it')"
apply (rule proper_it'I)
apply (simp add: comp_def)
apply (rule icf_proper_iteratorI)
apply (erule proper_it'D)
done
lemma proper_it_mono_dres_dom:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. f kv x ≤ f' kv x"
shows "
(map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f kv) σ
≤
(map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f' kv) σ"
apply (rule proper_it_mono_dres)
apply (rule icf_proper_iteratorI)
by fact+
lemma proper_it_mono_dres_dom_flat:
assumes PR: "proper_it' it it'"
assumes A: "⋀kv x. flat_ge (f kv x) (f' kv x)"
shows "flat_ge
((map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f kv) σ)
((map_iterator_dom o it') s (case_dres False False c) (λkv s. s ⤜ f' kv) σ)"
apply (rule proper_it_mono_dres_flat)
apply (rule icf_proper_iteratorI)
by fact+
lemmas proper_it_monos =
proper_it_mono_dres_pair proper_it_mono_dres_pair_flat
proper_it_mono_dres proper_it_mono_dres_flat
proper_it_mono_dres_dom proper_it_mono_dres_dom_flat
attribute_setup "proper_it" = ‹
Scan.succeed (Thm.declaration_attribute (fn thm => fn context =>
let
val mono_thms = map_filter (try (curry (RS) thm)) @{thms proper_it_monos}
val context = context
|> Icf_Proper_Iterator.add_thm thm
|> fold Refine_Mono_Prover.add_mono_thm mono_thms
in
context
end
))
›
"Proper iterator declaration"
end