Theory Implement
section ‹Implementation›
theory Implement
imports
"HOL-Library.Monad_Syntax"
"Collections.Refine_Dflt"
"Refine"
begin
subsection ‹Syntax›
no_syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" ("(2let _ =/ _)" [1000, 13] 13)
syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" ("(2let _ =/ _)" 13)
subsection ‹Monadic Refinement›
lemmas [refine] = plain_nres_relI
lemma vcg0:
assumes "(f, g) ∈ ⟨Id⟩ nres_rel"
shows "g ≤ h ⟹ f ≤ h"
using order_trans nres_relD[OF assms[param_fo, OF], THEN refine_IdD] by this
lemma vcg1:
assumes "(f, g) ∈ Id → ⟨Id⟩ nres_rel"
shows "g x ≤ h x ⟹ f x ≤ h x"
using order_trans nres_relD[OF assms[param_fo, OF IdI], THEN refine_IdD] by this
lemma vcg2:
assumes "(f, g) ∈ Id → Id → ⟨Id⟩ nres_rel"
shows "g x y ≤ h x y ⟹ f x y ≤ h x y"
using order_trans nres_relD[OF assms[param_fo, OF IdI IdI], THEN refine_IdD] by this
lemma RETURN_nres_relD:
assumes "(RETURN x, RETURN y) ∈ ⟨A⟩ nres_rel"
shows "(x, y) ∈ A"
using assms unfolding nres_rel_def by simp
lemma FOREACH_rule_insert:
assumes "finite S"
assumes "I {} s"
assumes "⋀ s. I S s ⟹ P s"
assumes "⋀ T x s. T ⊆ S ⟹ I T s ⟹ x ∈ S ⟹ x ∉ T ⟹ f x s ≤ SPEC (I (insert x T))"
shows "FOREACH S f s ≤ SPEC P"
proof (rule FOREACH_rule[where I = "λ T s. I (S - T) s"])
show "finite S" using assms(1) by this
show "I (S - S) s" using assms(2) by simp
show "P s" if "I (S - {}) s" for s using assms(3) that by simp
next
fix x T s
assume 1: "x ∈ T" "T ⊆ S" "I (S - T) s"
have "f x s ≤ SPEC (I (insert x (S - T)))" using assms(4) 1 by blast
also have "insert x (S - T) = S - (T - {x})" using 1(1, 2) by (simp add: it_step_insert_iff)
finally show "f x s ≤ SPEC (I (S - (T - {x})))" by this
qed
lemma FOREACH_rule_map:
assumes "finite (dom g)"
assumes "I Map.empty s"
assumes "⋀ s. I g s ⟹ P s"
assumes "⋀ h k v s. h ⊆⇩m g ⟹ I h s ⟹ g k = Some v ⟹ k ∉ dom h ⟹
f (k, v) s ≤ SPEC (I (h (k ↦ v)))"
shows "FOREACH (map_to_set g) f s ≤ SPEC P"
proof (rule FOREACH_rule_insert[where I = "λ H s. I (set_to_map H) s"])
show "finite (map_to_set g)" unfolding finite_map_to_set using assms(1) by this
show "I (set_to_map {}) s" using assms(2) by simp
show "P s" if "I (set_to_map (map_to_set g)) s" for s
using assms(3) that unfolding map_to_set_inverse by this
next
fix H x s
assume 1: "H ⊆ map_to_set g" "I (set_to_map H) s" "x ∈ map_to_set g" "x ∉ H"
obtain k v where 2: "x = (k, v)" by force
have 3: "inj_on fst H" using inj_on_fst_map_to_set inj_on_subset 1(1) by blast
have "f x s = f (k, v) s" unfolding 2 by rule
also have "… ≤ SPEC (I ((set_to_map H) (k ↦ v)))"
proof (rule assms(4))
show "set_to_map H ⊆⇩m g"
using 1(1) 3
by (metis inj_on_fst_map_to_set map_leI map_to_set_inverse set_to_map_simp subset_eq)
show "I (set_to_map H) s" using 1(2) by this
show "g k = Some v" using 1(3) unfolding 2 map_to_set_def by simp
show "k ∉ dom (set_to_map H)"
using 1(1, 3, 4) unfolding 2 set_to_map_dom
by (metis fst_conv inj_on_fst_map_to_set inj_on_image_mem_iff)
qed
also have "(set_to_map H) (k ↦ v) = (set_to_map H) (fst x ↦ snd x)" unfolding 2 by simp
also have "… = set_to_map (insert x H)"
using 1(1, 3, 4) by (metis inj_on_fst_map_to_set inj_on_image_mem_iff set_to_map_insert)
finally show "f x s ≤ SPEC (I (set_to_map (insert x H)))" by this
qed
lemma FOREACH_rule_insert_eq:
assumes "finite S"
assumes "X {} = s"
assumes "X S = t"
assumes "⋀ T x. T ⊆ S ⟹ x ∈ S ⟹ x ∉ T ⟹ f x (X T) ≤ SPEC (HOL.eq (X (insert x T)))"
shows "FOREACH S f s ≤ SPEC (HOL.eq t)"
by (rule FOREACH_rule_insert[where I = "HOL.eq ∘ X"]) (use assms in auto)
lemma FOREACH_rule_map_eq:
assumes "finite (dom g)"
assumes "X Map.empty = s"
assumes "X g = t"
assumes "⋀ h k v. h ⊆⇩m g ⟹ g k = Some v ⟹ k ∉ dom h ⟹
f (k, v) (X h) ≤ SPEC (HOL.eq (X (h (k ↦ v))))"
shows "FOREACH (map_to_set g) f s ≤ SPEC (HOL.eq t)"
by (rule FOREACH_rule_map[where I = "HOL.eq ∘ X"]) (use assms in auto)
lemma FOREACH_rule_map_map: "(FOREACH (map_to_set m) (λ (k, v). F k (f k v)),
FOREACH (map_to_set (λ k. map_option (f k) (m k))) (λ (k, v). F k v)) ∈ Id → ⟨Id⟩ nres_rel"
proof refine_vcg
show "inj_on (λ (k, v). (k, f k v)) (map_to_set m)"
unfolding map_to_set_def by rule auto
show "map_to_set (λ k. map_option (f k) (m k)) = (λ (k, v). (k, f k v)) ` map_to_set m"
unfolding map_to_set_def by auto
qed auto
subsection ‹Implementations for Sets Represented by Lists›
lemma list_set_rel_Id_on[simp]: "⟨Id_on A⟩ list_set_rel = ⟨Id⟩ list_set_rel ∩ UNIV × Pow A"
unfolding list_set_rel_def relcomp_unfold in_br_conv by auto
lemma list_set_card[param]: "(length, card) ∈ ⟨A⟩ list_set_rel → nat_rel"
unfolding list_set_rel_def relcomp_unfold in_br_conv
by (auto simp: distinct_card list_rel_imp_same_length)
lemma list_set_insert[param]:
assumes "y ∉ Y"
assumes "(x, y) ∈ A" "(xs, Y) ∈ ⟨A⟩ list_set_rel"
shows "(x # xs, insert y Y) ∈ ⟨A⟩ list_set_rel"
using assms unfolding list_set_rel_def relcomp_unfold in_br_conv
by (auto) (metis refine_list(2)[param_fo] distinct.simps(2) list.simps(15))
lemma list_set_union[param]:
assumes "X ∩ Y = {}"
assumes "(xs, X) ∈ ⟨A⟩ list_set_rel" "(ys, Y) ∈ ⟨A⟩ list_set_rel"
shows "(xs @ ys, X ∪ Y) ∈ ⟨A⟩ list_set_rel"
using assms unfolding list_set_rel_def relcomp_unfold in_br_conv
by (auto) (meson param_append[param_fo] distinct_append set_union_code)
lemma list_set_Union[param]:
assumes "⋀ X Y. X ∈ S ⟹ Y ∈ S ⟹ X ≠ Y ⟹ X ∩ Y = {}"
assumes "(xs, S) ∈ ⟨⟨A⟩ list_set_rel⟩ list_set_rel"
shows "(concat xs, Union S) ∈ ⟨A⟩ list_set_rel"
proof -
note distinct_map[iff]
obtain zs where 1: "(xs, zs) ∈ ⟨⟨A⟩ list_set_rel⟩ list_rel" "S = set zs" "distinct zs"
using assms(2) unfolding list_set_rel_def relcomp_unfold in_br_conv by auto
obtain ys where 2: "(xs, ys) ∈ ⟨⟨A⟩ list_rel⟩ list_rel" "zs = map set ys" "list_all distinct ys"
using 1(1)
unfolding list_set_rel_def list_rel_compp
unfolding relcomp_unfold mem_Collect_eq prod.case
unfolding br_list_rel in_br_conv
by auto
have 20: "set a ∈ S" "set b ∈ S" "set a ≠ set b" if "a ∈ set ys" "b ∈ set ys" "a ≠ b" for a b
using 1(3) that unfolding 1(2) 2(2) by (auto dest: inj_onD)
have 3: "set a ∩ set b = {}" if "a ∈ set ys" "b ∈ set ys" "a ≠ b" for a b
using assms(1) 20 that by auto
have 4: "Union S = set (concat ys)" unfolding 1(2) 2(2) by simp
have 5: "distinct (concat ys)"
using 1(3) 2(2, 3) 3 unfolding list.pred_set by (blast intro: distinct_concat)
have 6: "(concat xs, concat ys) ∈ ⟨A⟩ list_rel" using 2(1) by parametricity
show ?thesis unfolding list_set_rel_def relcomp_unfold in_br_conv using 4 5 6 by blast
qed
lemma list_set_image[param]:
assumes "inj_on g S"
assumes "(f, g) ∈ A → B" "(xs, S) ∈ ⟨A⟩ list_set_rel"
shows "(map f xs, g ` S) ∈ ⟨B⟩ list_set_rel"
using assms unfolding list_set_rel_def relcomp_unfold in_br_conv
using param_map[param_fo] distinct_map by fastforce
lemma list_set_bind[param]:
assumes "⋀ x y. x ∈ S ⟹ y ∈ S ⟹ x ≠ y ⟹ g x ∩ g y = {}"
assumes "(xs, S) ∈ ⟨A⟩ list_set_rel" "(f, g) ∈ A → ⟨B⟩ list_set_rel"
shows "(xs ⤜ f, S ⤜ g) ∈ ⟨B⟩ list_set_rel"
proof -
note [param] = list_set_autoref_filter list_set_autoref_isEmpty
let ?xs = "filter (Not ∘ is_Nil ∘ f) xs"
let ?S = "op_set_filter (Not ∘ op_set_isEmpty ∘ g) S"
have 1: "inj_on g ?S" using assms(1) by (fastforce intro: inj_onI)
have "xs ⤜ f = concat (map f ?xs)" by (induct xs) (auto split: list.split)
also have "(…, ⋃ (g ` ?S)) ∈ ⟨B⟩ list_set_rel" using assms 1 by parametricity auto
also have "⋃ (g ` ?S) = S ⤜ g" by auto auto
finally show ?thesis by this
qed
subsection ‹Autoref Setup›
lemma dflt_ahm_rel_finite_nat: "finite_map_rel (⟨nat_rel, V⟩ dflt_ahm_rel)" by tagged_solver
context
begin
interpretation autoref_syn by this
lemma [autoref_op_pat]: "(Some ∘ f) |` X ≡ OP (λ f X. (Some ∘ f) |` X) f X" by simp
lemma [autoref_op_pat]: "⋃(m ` S) ≡ OP (λS m. ⋃(m ` S)) S m" by simp
definition gen_UNION where
"gen_UNION tol emp un X f ≡ fold (un ∘ f) (tol X) emp"
lemma gen_UNION[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes to_list: "SIDE_GEN_ALGO (is_set_to_list A Rs1 tol)"
assumes empty: "GEN_OP emp {} (⟨B⟩ Rs3)"
assumes union: "GEN_OP un union (⟨B⟩ Rs2 → ⟨B⟩ Rs3 → ⟨B⟩ Rs3)"
shows "(gen_UNION tol emp un, λA f. ⋃ (f ` A)) ∈ ⟨A⟩ Rs1 → (A → ⟨B⟩ Rs2) → ⟨B⟩ Rs3"
proof (intro fun_relI)
note [unfolded autoref_tag_defs, param] = empty union
fix f g T S
assume 1[param]: "(T, S) ∈ ⟨A⟩ Rs1" "(g, f) ∈ A → ⟨B⟩ Rs2"
obtain tsl' where
[param]: "(tol T, tsl') ∈ ⟨A⟩ list_rel"
and IT': "RETURN tsl' ≤ it_to_sorted_list (λ_ _. True) S"
using to_list[unfolded autoref_tag_defs is_set_to_list_def] 1(1)
by (rule is_set_to_sorted_listE)
from IT' have 10: "S = set tsl'" "distinct tsl'" unfolding it_to_sorted_list_def by simp_all
have "gen_UNION tol emp un T g = fold (un ∘ g) (tol T) emp" unfolding gen_UNION_def by rule
also have "(…, fold (union ∘ f) tsl' {}) ∈ ⟨B⟩ Rs3" by parametricity
also have "fold (union ∘ f) tsl' X = ⋃(f ` S) ∪ X" for X
unfolding 10(1) by (induct tsl' arbitrary: X) (auto)
also have "⋃(f ` S) ∪ {} = ⋃(f ` S)" by simp
finally show "(gen_UNION tol emp un T g, ⋃(f ` S)) ∈ ⟨B⟩ Rs3" by this
qed
definition gen_Image where
"gen_Image tol1 mem2 emp3 ins3 X Y ≡ fold
(λ (a, b). if mem2 a Y then ins3 b else id) (tol1 X) emp3"
lemma gen_Image[autoref_rules]:
assumes PRIO_TAG_GEN_ALGO
assumes to_list: "SIDE_GEN_ALGO (is_set_to_list (A ×⇩r B) Rs1 tol1)"
assumes member: "GEN_OP mem2 (∈) (A → ⟨A⟩ Rs2 → bool_rel)"
assumes empty: "GEN_OP emp3 {} (⟨B⟩ Rs3)"
assumes insert: "GEN_OP ins3 Set.insert (B → ⟨B⟩ Rs3 → ⟨B⟩ Rs3)"
shows "(gen_Image tol1 mem2 emp3 ins3, Image) ∈ ⟨A ×⇩r B⟩ Rs1 → ⟨A⟩ Rs2 → ⟨B⟩ Rs3"
proof (intro fun_relI)
note [unfolded autoref_tag_defs, param] = member empty insert
fix T S X Y
assume 1[param]: "(T, S) ∈ ⟨A ×⇩r B⟩ Rs1" "(Y, X) ∈ ⟨A⟩ Rs2"
obtain tsl' where
[param]: "(tol1 T, tsl') ∈ ⟨A ×⇩r B⟩ list_rel"
and IT': "RETURN tsl' ≤ it_to_sorted_list (λ_ _. True) S"
using to_list[unfolded autoref_tag_defs is_set_to_list_def] 1(1)
by (rule is_set_to_sorted_listE)
from IT' have 10: "S = set tsl'" "distinct tsl'" unfolding it_to_sorted_list_def by simp_all
have "gen_Image tol1 mem2 emp3 ins3 T Y =
fold (λ (a, b). if mem2 a Y then ins3 b else id) (tol1 T) emp3"
unfolding gen_Image_def by rule
also have "(…, fold (λ (a, b). if a ∈ X then Set.insert b else id) tsl' {}) ∈ ⟨B⟩ Rs3"
by parametricity
also have "fold (λ (a, b). if a ∈ X then Set.insert b else id) tsl' M = S `` X ∪ M" for M
unfolding 10(1) by (induct tsl' arbitrary: M) (auto split: prod.splits)
also have "S `` X ∪ {} = S `` X" by simp
finally show "(gen_Image tol1 mem2 emp3 ins3 T Y, S `` X) ∈ ⟨B⟩ Rs3" by this
qed
lemma list_set_union_autoref[autoref_rules]:
assumes "PRIO_TAG_OPTIMIZATION"
assumes "SIDE_PRECOND_OPT (a' ∩ b' = {})"
assumes "(a, a') ∈ ⟨R⟩ list_set_rel"
assumes "(b, b') ∈ ⟨R⟩ list_set_rel"
shows "(a @ b,
(OP union ::: ⟨R⟩ list_set_rel → ⟨R⟩ list_set_rel → ⟨R⟩ list_set_rel) $ a' $ b') ∈
⟨R⟩ list_set_rel"
using assms list_set_union unfolding autoref_tag_defs by blast
lemma list_set_image_autoref[autoref_rules]:
assumes "PRIO_TAG_OPTIMIZATION"
assumes INJ: "SIDE_PRECOND_OPT (inj_on f s)"
assumes "⋀ xi x. (xi, x) ∈ Ra ⟹ x ∈ s ⟹ (fi xi, f $ x) ∈ Rb"
assumes LP: "(l,s)∈⟨Ra⟩list_set_rel"
shows "(map fi l,
(OP image ::: (Ra → Rb) → ⟨Ra⟩ list_set_rel → ⟨Rb⟩ list_set_rel) $ f $ s) ∈
⟨Rb⟩ list_set_rel"
proof -
from LP obtain l' where 1: "(l,l')∈⟨Ra⟩list_rel" and L'S: "(l',s)∈br set distinct"
unfolding list_set_rel_def by auto
have 2: "s = set l'" using L'S unfolding in_br_conv by auto
have "(map fi l, map f l')∈⟨Rb⟩list_rel"
using 1 L'S assms(3) unfolding 2 in_br_conv by induct auto
also from INJ L'S have "(map f l',f`s)∈br set distinct"
by (induct l' arbitrary: s) (auto simp: br_def dest: injD)
finally (relcompI) show ?thesis unfolding autoref_tag_defs list_set_rel_def by this
qed
lemma list_set_UNION_autoref[autoref_rules]:
assumes "PRIO_TAG_OPTIMIZATION"
assumes "SIDE_PRECOND_OPT (∀ x ∈ S. ∀ y ∈ S. x ≠ y ⟶ g x ∩ g y = {})"
assumes "(xs, S) ∈ ⟨A⟩ list_set_rel" "(f, g) ∈ A → ⟨B⟩ list_set_rel"
shows "(xs ⤜ f,
(OP (λA f. ⋃ (f ` A)) ::: ⟨A⟩ list_set_rel → (A → ⟨B⟩ list_set_rel) → ⟨B⟩ list_set_rel) $ S $ g) ∈
⟨B⟩ list_set_rel"
using assms list_set_bind unfolding bind_UNION autoref_tag_defs by metis
definition gen_equals where
"gen_equals ball lu eq f g ≡
ball f (λ (k, v). rel_option eq (lu k g) (Some v)) ∧
ball g (λ (k, v). rel_option eq (lu k f) (Some v))"
lemma gen_equals[autoref_rules]:
assumes PRIO_TAG_GEN_ALGO
assumes BALL: "GEN_OP ball op_map_ball (⟨Rk, Rv⟩ Rm → (Rk ×⇩r Rv → bool_rel) → bool_rel)"
assumes LU: "GEN_OP lu op_map_lookup (Rk → ⟨Rk, Rv⟩ Rm → ⟨Rv⟩ option_rel)"
assumes EQ: "GEN_OP eq HOL.eq (Rv → Rv → bool_rel)"
shows "(gen_equals ball lu eq, HOL.eq) ∈ ⟨Rk, Rv⟩ Rm → ⟨Rk, Rv⟩ Rm → bool_rel"
proof (intro fun_relI)
note [unfolded autoref_tag_defs, param] = BALL LU EQ
fix fi f gi g
assume [param]: "(fi, f) ∈ ⟨Rk, Rv⟩ Rm" "(gi, g) ∈ ⟨Rk, Rv⟩ Rm"
have "gen_equals ball lu eq fi gi ⟷ ball fi (λ (k, v). rel_option eq (lu k gi) (Some v)) ∧
ball gi (λ (k, v). rel_option eq (lu k fi) (Some v))"
unfolding gen_equals_def by rule
also have "ball fi (λ (k, v). rel_option eq (lu k gi) (Some v)) ⟷
op_map_ball f (λ (k, v). rel_option HOL.eq (op_map_lookup k g) (Some v))"
by (rule IdD) (parametricity)
also have "ball gi (λ (k, v). rel_option eq (lu k fi) (Some v)) ⟷
op_map_ball g (λ (k, v). rel_option HOL.eq (op_map_lookup k f) (Some v))"
by (rule IdD) (parametricity)
also have "op_map_ball f (λ (k, v). rel_option HOL.eq (op_map_lookup k g) (Some v)) ∧
op_map_ball g (λ (k, v). rel_option HOL.eq (op_map_lookup k f) (Some v)) ⟷
(∀ a b. f a = Some b ⟷ g a = Some b)"
unfolding op_map_ball_def map_to_set_def option.rel_eq op_map_lookup_def by auto
also have "(∀ a b. f a = Some b ⟷ g a = Some b) ⟷ f = g" using option.exhaust ext by metis
finally show "(gen_equals ball lu eq fi gi, f = g) ∈ bool_rel" by simp
qed
definition op_set_enumerate :: "'a set ⇒ ('a ⇀ nat) nres" where
"op_set_enumerate S ≡ SPEC (λ f. dom f = S ∧ inj_on f S)"
lemma [autoref_itype]: "op_set_enumerate ::⇩i ⟨A⟩⇩i i_set →⇩i ⟨⟨A, i_nat⟩⇩i i_map⟩⇩i i_nres" by simp
lemma [autoref_hom]: "CONSTRAINT op_set_enumerate (⟨A⟩ Rs → ⟨⟨A, nat_rel⟩ Rm⟩ nres_rel)" by simp
definition gen_enumerate where
"gen_enumerate tol upd emp S ≡ snd (fold (λ x (k, m). (Suc k, upd x k m)) (tol S) (0, emp))"
lemma gen_enumerate[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes to_list: "SIDE_GEN_ALGO (is_set_to_list A Rs tol)"
assumes empty: "GEN_OP emp op_map_empty (⟨A, nat_rel⟩ Rm)"
assumes update: "GEN_OP upd op_map_update (A → nat_rel → ⟨A, nat_rel⟩ Rm → ⟨A, nat_rel⟩ Rm)"
shows "(λ S. RETURN (gen_enumerate tol upd emp S), op_set_enumerate) ∈
⟨A⟩ Rs → ⟨⟨A, nat_rel⟩ Rm⟩ nres_rel"
proof
note [unfolded autoref_tag_defs, param] = empty update
fix T S
assume 1: "(T, S) ∈ ⟨A⟩ Rs"
obtain tsl' where
[param]: "(tol T, tsl') ∈ ⟨A⟩list_rel"
and IT': "RETURN tsl' ≤ it_to_sorted_list (λ_ _. True) S"
using to_list[unfolded autoref_tag_defs is_set_to_list_def] 1
by (rule is_set_to_sorted_listE)
from IT' have 10: "S = set tsl'" "distinct tsl'" unfolding it_to_sorted_list_def by simp_all
have 2: "dom (snd (fold (λ x (k, m). (Suc k, m (x ↦ k))) tsl' (k, m))) = dom m ∪ set tsl'"
for k m by (induct tsl' arbitrary: k m) (auto)
have 3: "inj_on (snd (fold (λ x (k, m). (Suc k, m (x ↦ k))) tsl' (0, Map.empty))) (set tsl')"
using 10(2) by (auto intro!: inj_onI simp: fold_map_of)
(metis diff_zero distinct_Ex1 distinct_upt length_upt map_of_zip_nth option.simps(1))
let ?f = "RETURN (snd (fold (λ x (k, m). (Suc k, op_map_update x k m)) tsl' (0, op_map_empty)))"
have "(RETURN (gen_enumerate tol upd emp T), ?f) ∈ ⟨⟨A, nat_rel⟩ Rm⟩ nres_rel"
unfolding gen_enumerate_def by parametricity
also have "(?f, op_set_enumerate S) ∈ ⟨Id⟩ nres_rel"
unfolding op_set_enumerate_def using 2 3 10 by refine_vcg auto
finally show "(RETURN (gen_enumerate tol upd emp T), op_set_enumerate S) ∈
⟨⟨A, nat_rel⟩ Rm⟩ nres_rel" unfolding nres_rel_comp by simp
qed
lemma gen_enumerate_it_to_list[refine_transfer_post_simp]:
"gen_enumerate (it_to_list it) =
(λ upd emp S. snd (foldli (it_to_list it S) (λ _. True)
(λ x s. case s of (k, m) ⇒ (Suc k, upd x k m)) (0, emp)))"
unfolding gen_enumerate_def
unfolding foldl_conv_fold[symmetric]
unfolding foldli_foldl[symmetric]
by rule
definition gen_build where
"gen_build tol upd emp f X ≡ fold (λ x. upd x (f x)) (tol X) emp"
lemma gen_build[autoref_rules]:
assumes PRIO_TAG_GEN_ALGO
assumes to_list: "SIDE_GEN_ALGO (is_set_to_list A Rs tol)"
assumes empty: "GEN_OP emp op_map_empty (⟨A, B⟩ Rm)"
assumes update: "GEN_OP upd op_map_update (A → B → ⟨A, B⟩ Rm → ⟨A, B⟩ Rm)"
shows "(λ f X. gen_build tol upd emp f X, λ f X. (Some ∘ f) |` X) ∈
(A → B) → ⟨A⟩ Rs → ⟨A, B⟩ Rm"
proof (intro fun_relI)
note [unfolded autoref_tag_defs, param] = empty update
fix f g T S
assume 1[param]: "(g, f) ∈ A → B" "(T, S) ∈ ⟨A⟩ Rs"
obtain tsl' where
[param]: "(tol T, tsl') ∈ ⟨A⟩list_rel"
and IT': "RETURN tsl' ≤ it_to_sorted_list (λ_ _. True) S"
using to_list[unfolded autoref_tag_defs is_set_to_list_def] 1(2)
by (rule is_set_to_sorted_listE)
from IT' have 10: "S = set tsl'" "distinct tsl'" unfolding it_to_sorted_list_def by simp_all
have "gen_build tol upd emp g T = fold (λ x. upd x (g x)) (tol T) emp"
unfolding gen_build_def by rule
also have "(…, fold (λ x. op_map_update x (f x)) tsl' op_map_empty) ∈ ⟨A, B⟩ Rm"
by parametricity
also have "fold (λ x. op_map_update x (f x)) tsl' m = m ++ (Some ∘ f) |` S" for m
unfolding 10 op_map_update_def
by (induct tsl' arbitrary: m rule: rev_induct) (auto simp add: restrict_map_insert)
also have "op_map_empty ++ (Some ∘ f) |` S = (Some ∘ f) |` S" by simp
finally show "(gen_build tol upd emp g T, (Some ∘ f) |` S) ∈ ⟨A, B⟩ Rm" by this
qed
definition "to_list it s ≡ it s top Cons Nil"
lemma map2set_to_list:
assumes "GEN_ALGO_tag (is_map_to_list Rk unit_rel R it)"
shows "is_set_to_list Rk (map2set_rel R) (to_list (map_iterator_dom ∘ (foldli ∘ it)))"
unfolding is_set_to_list_def is_set_to_sorted_list_def
proof safe
fix f g
assume 1: "(f, g) ∈ ⟨Rk⟩ map2set_rel R"
obtain xs where 2: "(it_to_list (map_iterator_dom ∘ (foldli ∘ it)) f, xs) ∈ ⟨Rk⟩ list_rel"
"RETURN xs ≤ it_to_sorted_list (λ _ _. True) g"
using map2set_to_list[OF assms] 1
unfolding is_set_to_list_def is_set_to_sorted_list_def
by auto
have 3: "map_iterator_dom (foldli xs) top (#) a =
rev (map_iterator_dom (foldli xs) (λ _. True) (λ x l. l @ [x]) (rev a))"
for xs :: "('k × unit) list" and a
unfolding map_iterator_dom_def set_iterator_image_def set_iterator_image_filter_def
by (induct xs arbitrary: a) (auto)
show "∃ xs. (to_list (map_iterator_dom ∘ (foldli ∘ it)) f, xs) ∈ ⟨Rk⟩ list_rel ∧
RETURN xs ≤ it_to_sorted_list (λ _ _. True) g"
proof (intro exI conjI)
have "to_list (map_iterator_dom ∘ (foldli ∘ it)) f =
rev (it_to_list (map_iterator_dom ∘ (foldli ∘ it)) f)"
unfolding to_list_def it_to_list_def by (simp add: 3)
also have "(rev (it_to_list (map_iterator_dom ∘ (foldli ∘ it)) f), rev xs) ∈ ⟨Rk⟩ list_rel"
using 2(1) by parametricity
finally show "(to_list (map_iterator_dom ∘ (foldli ∘ it)) f, rev xs) ∈ ⟨Rk⟩ list_rel" by this
show "RETURN (rev xs) ≤ it_to_sorted_list (λ _ _. True) g"
using 2(2) unfolding it_to_sorted_list_def by auto
qed
qed
lemma CAST_to_list[autoref_rules_raw]:
assumes PRIO_TAG_GEN_ALGO
assumes "SIDE_GEN_ALGO (is_set_to_list A Rs tol)"
shows "(tol, CAST) ∈ ⟨A⟩ Rs → ⟨A⟩ list_set_rel"
using assms(2) unfolding autoref_tag_defs is_set_to_list_def
by (auto simp: it_to_sorted_list_def list_set_rel_def in_br_conv elim!: is_set_to_sorted_listE)
lemma param_foldli:
assumes "(xs, ys) ∈ ⟨Ra⟩ list_rel"
assumes "(c, d) ∈ Rs → bool_rel"
assumes "⋀ x y. (x, y) ∈ Ra ⟹ x ∈ set xs ⟹ y ∈ set ys ⟹ (f x, g y) ∈ Rs → Rs"
assumes "(a, b) ∈ Rs"
shows "(foldli xs c f a, foldli ys d g b) ∈ Rs"
using assms
proof (induct arbitrary: a b)
case 1
then show ?case by simp
next
case (2 x y xs ys)
show ?case
proof (cases "c a")
case True
have 10: "(c a, d b) ∈ bool_rel" using 2 by parametricity
have 20: "d b" using 10 True by auto
have 30: "(foldli xs c f (f x a), foldli ys d g (g y b)) ∈ Rs"
by (auto intro!: 2 2(5)[THEN fun_relD])
show ?thesis using True 20 30 by simp
next
case False
have 10: "(c a, d b) ∈ bool_rel" using 2 by parametricity
have 20: "¬ d b" using 10 False by auto
show ?thesis unfolding foldli.simps using False 20 2 by simp
qed
qed
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]: "⋀ x y. (x, y) ∈ Rk ⟹ y ∈ s' ⟹ (f x,f' y)∈Rσ → Rσ"
assumes [param]: "(σ,σ')∈Rσ"
shows "(foldli (tsl s) c f σ, result s') ∈ Rσ"
proof -
obtain tsl' where
n[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)
from IT have suen: "s' = set tsl'"
unfolding it_to_sorted_list_def by simp_all
have "(foldli (tsl s) c f σ, foldli tsl' c' f' σ') ∈ Rσ"
using assms(4, 5, 6) n unfolding suen
using param_foldli[OF n assms(4)] assms by simp
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 "⋀ x y. (x, y) ∈ Rk ⟹ y ∈ s' ⟹ (f x, f' y)∈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)
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)"
assumes "⋀ xi x. (xi, x) ∈ Rk ⟹ x ∈ s ⟹ (fi xi, f $ x) ∈ Rk'"
assumes "(l, s) ∈ ⟨Rk⟩Rs1"
shows "(gen_image (λ x. foldli (it1 x)) empty2 ins2 fi l,
(OP image ::: (Rk→Rk') → (⟨Rk⟩Rs1) → (⟨Rk'⟩Rs2)) $ f $ s) ∈ (⟨Rk'⟩Rs2)"
proof -
note [unfolded autoref_tag_defs, param] = INS EMPTY
note 1 = det_fold_set[OF foldli_image IT[unfolded autoref_tag_defs]]
show ?thesis using assms 1 unfolding gen_image_def autoref_tag_defs by parametricity
qed
end
end