# Theory Impl_List_Set

```section ‹\isaheader{List Based Sets}›
theory Impl_List_Set
imports
"../../Iterator/Iterator"
"../Intf/Intf_Set"
begin
(* TODO: Move *)
lemma list_all2_refl_conv:
"list_all2 P xs xs ⟷ (∀x∈set xs. P x x)"
by (induct xs) auto

primrec glist_member :: "('a⇒'a⇒bool) ⇒ 'a ⇒ 'a list ⇒ bool" where
"glist_member eq x [] ⟷ False"
| "glist_member eq x (y#ys) ⟷ eq x y ∨ glist_member eq x ys"

lemma param_glist_member[param]:
"(glist_member,glist_member)∈(Ra→Ra→Id) → Ra → ⟨Ra⟩list_rel → Id"
unfolding glist_member_def
by (parametricity)

lemma list_member_alt: "List.member = (λl x. glist_member (=) x l)"
proof (intro ext)
fix x l
show "List.member l x = glist_member (=) x l"
by (induct l) (auto simp: List.member_rec)
qed

thm List.insert_def
definition
"glist_insert eq x xs = (if glist_member eq x xs then xs else x#xs)"

lemma param_glist_insert[param]:
"(glist_insert, glist_insert) ∈ (R→R→Id) → R → ⟨R⟩list_rel → ⟨R⟩list_rel"
unfolding glist_insert_def[abs_def]
by (parametricity)

primrec rev_append where
"rev_append [] ac = ac"
| "rev_append (x#xs) ac = rev_append xs (x#ac)"

lemma rev_append_eq: "rev_append l ac = rev l @ ac"
by (induct l arbitrary: ac) auto

(*
primrec glist_delete_aux1 :: "('a⇒'a⇒bool) ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"glist_delete_aux1 eq x [] = []"
| "glist_delete_aux1 eq x (y#ys) = (
if eq x y then
ys
else y#glist_delete_aux1 eq x ys)"

primrec glist_delete_aux2 :: "('a⇒'a⇒_) ⇒ _" where
"glist_delete_aux2 eq ac x [] = ac"
| "glist_delete_aux2 eq ac x (y#ys) = (if eq x y then rev_append ys ac else
glist_delete_aux2 eq (y#ac) x ys
)"

lemma glist_delete_aux2_eq1:
"glist_delete_aux2 eq ac x l = rev (glist_delete_aux1 eq x l) @ ac"
by (induct l arbitrary: ac) (auto simp: rev_append_eq)

definition "glist_delete eq x l = glist_delete_aux2 eq [] x l"
*)

primrec glist_delete_aux :: "('a ⇒ 'a ⇒ bool) ⇒ _" where
"glist_delete_aux eq x [] as = as"
| "glist_delete_aux eq x (y#ys) as = (
if eq x y then rev_append as ys
else glist_delete_aux eq x ys (y#as)
)"

definition glist_delete where
"glist_delete eq x l ≡ glist_delete_aux eq x l []"

lemma param_glist_delete[param]:
"(glist_delete, glist_delete) ∈ (R→R→Id) → R → ⟨R⟩list_rel → ⟨R⟩list_rel"
unfolding glist_delete_def[abs_def]
glist_delete_aux_def
rev_append_def
by (parametricity)

lemma list_rel_Range:
"∀x'∈set l'. x' ∈ Range R ⟹ l' ∈ Range (⟨R⟩list_rel)"
proof (induction l')
case Nil thus ?case by force
next
case (Cons x' xs')
then obtain xs where "(xs,xs') ∈ ⟨R⟩ list_rel" by force
moreover from Cons.prems obtain x where "(x,x') ∈ R" by force
ultimately have "(x#xs, x'#xs') ∈ ⟨R⟩ list_rel" by simp
thus ?case ..
qed

text ‹All finite sets can be represented›
lemma list_set_rel_range:
"Range (⟨R⟩list_set_rel) = { S. finite S ∧ S⊆Range R }"
(is "?A = ?B")
proof (intro equalityI subsetI)
fix s' assume "s' ∈ ?A"
then obtain l l' where A: "(l,l') ∈ ⟨R⟩list_rel" and
B: "s' = set l'" and C: "distinct l'"
unfolding list_set_rel_def br_def by blast
moreover have "set l' ⊆ Range R"
by (induction rule: list_rel_induct[OF A], auto)
ultimately show "s' ∈ ?B" by simp
next
fix s' assume A: "s' ∈ ?B"
then obtain l' where B: "set l' = s'" and C: "distinct l'"
using finite_distinct_list by blast
hence "(l',s') ∈ br set distinct" by (simp add: br_def)

moreover from A and B have "∀x∈set l'. x ∈ Range R" by blast
from list_rel_Range[OF this] obtain l
where "(l,l') ∈ ⟨R⟩list_rel" by blast

ultimately show "s' ∈ ?A" unfolding list_set_rel_def by fast
qed

lemmas [autoref_rel_intf] = REL_INTFI[of list_set_rel i_set]

lemma list_set_rel_finite[autoref_ga_rules]:
"finite_set_rel (⟨R⟩list_set_rel)"
unfolding finite_set_rel_def list_set_rel_def
by (auto simp: br_def)

lemma list_set_rel_sv[relator_props]:
"single_valued R ⟹ single_valued (⟨R⟩list_set_rel)"
unfolding list_set_rel_def
by tagged_solver

(* TODO: Move to Misc *)
lemma Id_comp_Id: "Id O Id = Id" by simp

lemma glist_member_id_impl:
"(glist_member (=), (∈)) ∈ Id → br set distinct → Id"
proof (intro fun_relI, goal_cases)
case (1 x x' l s') thus ?case
by (induct l arbitrary: s') (auto simp: br_def)
qed

lemma glist_insert_id_impl:
"(glist_insert (=), Set.insert) ∈ Id → br set distinct → br set distinct"
proof -
have IC: "⋀x s. insert x s = (if x∈s then s else insert x s)" by auto

show ?thesis
apply (intro fun_relI)
apply (subst IC)
unfolding glist_insert_def
apply (auto simp: br_def)
done
qed

lemma glist_delete_id_impl:
"(glist_delete (=), λx s. s-{x})
∈ Id→br set distinct → br set distinct"
proof (intro fun_relI)
fix x x':: 'a and s and s' :: "'a set"
assume XREL: "(x, x') ∈ Id" and SREL: "(s, s') ∈ br set distinct"
from XREL have [simp]: "x'=x" by simp

{
fix a and a' :: "'a set"
assume "(a,a')∈br set distinct" and "s' ∩ a' = {}"
hence "(glist_delete_aux (=) x s a, s'-{x'} ∪ a')∈br set distinct"
using SREL
proof (induction s arbitrary: a s' a')
case Nil thus ?case by (simp add: br_def)
next
case (Cons y s)
show ?case proof (cases "x=y")
case True with Cons show ?thesis
by (auto simp add: br_def rev_append_eq)
next
case False
have "glist_delete_aux (=) x (y # s) a
= glist_delete_aux (=) x s (y#a)" by (simp add: False)
also have "(…,set s - {x'} ∪ insert y a')∈br set distinct"
apply (rule Cons.IH[of "y#a" "insert y a'" "set s"])
using Cons.prems by (auto simp: br_def)
also have "set s - {x'} ∪ insert y a' = (s' - {x'}) ∪ a'"
proof -
from Cons.prems have [simp]: "s' = insert y (set s)"
by (auto simp: br_def)
show ?thesis using False by auto
qed
finally show ?thesis .
qed
qed
}
from this[of "[]" "{}"]
show "(glist_delete (=) x s, s' - {x'}) ∈ br set distinct"
unfolding glist_delete_def
qed

lemma list_set_autoref_empty[autoref_rules]:
"([],{})∈⟨R⟩list_set_rel"
by (auto simp: list_set_rel_def br_def)

lemma list_set_autoref_member[autoref_rules]:
assumes "GEN_OP eq (=) (R→R→Id)"
shows "(glist_member eq,(∈)) ∈ R → ⟨R⟩list_set_rel → Id"
using assms
apply (intro fun_relI)
unfolding list_set_rel_def
apply (erule relcompE)
apply (simp del: pair_in_Id_conv)
apply (subst Id_comp_Id[symmetric])
apply (rule relcompI[rotated])
apply (rule glist_member_id_impl[param_fo])
apply (rule IdI)
apply assumption
apply parametricity
done

lemma list_set_autoref_insert[autoref_rules]:
assumes "GEN_OP eq (=) (R→R→Id)"
shows "(glist_insert eq,Set.insert)
∈ R → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
using assms
apply (intro fun_relI)
unfolding list_set_rel_def
apply (erule relcompE)
apply (simp del: pair_in_Id_conv)
apply (rule relcompI[rotated])
apply (rule glist_insert_id_impl[param_fo])
apply (rule IdI)
apply assumption
apply parametricity
done

lemma list_set_autoref_delete[autoref_rules]:
assumes "GEN_OP eq (=) (R→R→Id)"
shows "(glist_delete eq,op_set_delete)
∈ R → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
using assms
apply (intro fun_relI)
unfolding list_set_rel_def
apply (erule relcompE)
apply (simp del: pair_in_Id_conv)
apply (rule relcompI[rotated])
apply (rule glist_delete_id_impl[param_fo])
apply (rule IdI)
apply assumption
apply parametricity
done

lemma list_set_autoref_to_list[autoref_ga_rules]:
shows "is_set_to_sorted_list (λ_ _. True) R list_set_rel id"
unfolding is_set_to_list_def is_set_to_sorted_list_def
it_to_sorted_list_def list_set_rel_def br_def
by auto

lemma list_set_it_simp[refine_transfer_post_simp]:
"foldli (id l) = foldli l" by simp

lemma glist_insert_dj_id_impl:
"⟦ x∉s; (l,s)∈br set distinct ⟧ ⟹ (x#l,insert x s)∈br set distinct"
by (auto simp: br_def)

context begin interpretation autoref_syn .
lemma list_set_autoref_insert_dj[autoref_rules]:
assumes "PRIO_TAG_OPTIMIZATION"
assumes "SIDE_PRECOND_OPT (x'∉s')"
assumes "(x,x')∈R"
assumes "(s,s')∈⟨R⟩list_set_rel"
shows "(x#s,
(OP Set.insert ::: R → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel) \$ x' \$ s')
∈ ⟨R⟩list_set_rel"
using assms
unfolding autoref_tag_defs
unfolding list_set_rel_def
apply -
apply (erule relcompE)
apply (simp del: pair_in_Id_conv)
apply (rule relcompI[rotated])
apply (rule glist_insert_dj_id_impl)
apply assumption
apply assumption
apply parametricity
done
end

subsection ‹More Operations›
lemma list_set_autoref_isEmpty[autoref_rules]:
"(is_Nil,op_set_isEmpty) ∈ ⟨R⟩list_set_rel → bool_rel"
by (auto simp: list_set_rel_def br_def split: list.split_asm)

lemma list_set_autoref_filter[autoref_rules]:
"(filter,op_set_filter)
∈ (R → bool_rel) → ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
proof -
have "(filter, op_set_filter)
∈ (Id → bool_rel) → ⟨Id⟩list_set_rel → ⟨Id⟩list_set_rel"
by (auto simp: list_set_rel_def br_def)
note this[param_fo]
moreover have "(filter,filter)∈(R → bool_rel) → ⟨R⟩list_rel → ⟨R⟩list_rel"
unfolding List.filter_def
by parametricity
note this[param_fo]
ultimately show ?thesis
unfolding list_set_rel_def
apply (intro fun_relI)
apply (erule relcompE, simp)
apply (rule relcompI)
apply (rprems, assumption+)
apply (rprems, simp+)
done
qed

context begin interpretation autoref_syn .
lemma list_set_autoref_inj_image[autoref_rules]:
assumes "PRIO_TAG_OPTIMIZATION"
assumes INJ: "SIDE_PRECOND_OPT (inj_on f s)"
assumes [param]: "(fi,f)∈Ra→Rb"
assumes LP: "(l,s)∈⟨Ra⟩list_set_rel"
shows "(map fi l,
(OP (`) ::: (Ra→Rb) → ⟨Ra⟩list_set_rel → ⟨Rb⟩list_set_rel)\$f\$s)
∈ ⟨Rb⟩list_set_rel"
proof -
from LP obtain l' where
[param]: "(l,l')∈⟨Ra⟩list_rel" and L'S: "(l',s)∈br set distinct"
unfolding list_set_rel_def by auto

have "(map fi l, map f l')∈⟨Rb⟩list_rel" by parametricity
also from INJ L'S have "(map f l',f`s)∈br set distinct"
apply (induction l' arbitrary: s)
apply (auto simp: br_def dest: injD)
done
finally (relcompI) show ?thesis
unfolding autoref_tag_defs list_set_rel_def .
qed

end

lemma list_set_cart_autoref[autoref_rules]:
fixes Rx :: "('xi × 'x) set"
fixes Ry :: "('yi × 'y) set"
shows "(λxl yl. [ (x,y). x←xl, y←yl], op_set_cart)
∈ ⟨Rx⟩list_set_rel → ⟨Ry⟩list_set_rel → ⟨Rx ×⇩r Ry⟩list_set_rel"
proof (intro fun_relI)
fix xl xs yl ys
assume "(xl, xs) ∈ ⟨Rx⟩list_set_rel" "(yl, ys) ∈ ⟨Ry⟩list_set_rel"
then obtain xl' :: "'x list" and yl' :: "'y list" where
[param]: "(xl,xl')∈⟨Rx⟩list_rel" "(yl,yl')∈⟨Ry⟩list_rel"
and XLS: "(xl',xs)∈br set distinct" and YLS: "(yl',ys)∈br set distinct"
unfolding list_set_rel_def
by auto

have "([ (x,y). x←xl, y←yl ], [ (x,y). x←xl', y←yl' ])
∈ ⟨Rx ×⇩r Ry⟩list_rel"
by parametricity
also have "([ (x,y). x←xl', y←yl' ], xs × ys) ∈ br set distinct"
using XLS YLS
apply (auto simp: br_def)
apply hypsubst_thin
apply (induction xl')
apply simp
apply (induction yl')
apply simp
apply auto []
apply (metis (lifting) concat_map_maps distinct.simps(2)
distinct_singleton maps_simps(2))
done
finally (relcompI)
show "([ (x,y). x←xl, y←yl ], op_set_cart xs ys) ∈ ⟨Rx ×⇩r Ry⟩list_set_rel"
unfolding list_set_rel_def by simp
qed

subsection ‹Optimizations›
lemma glist_delete_hd: "eq x y ⟹ glist_delete eq x (y#s) = s"

text ‹Hack to ensure specific ordering. Note that ordering has no meaning
abstractly›
definition [simp]: "LIST_SET_REV_TAG ≡ λx. x"

lemma LIST_SET_REV_TAG_autoref[autoref_rules]:
"(rev,LIST_SET_REV_TAG) ∈ ⟨R⟩list_set_rel → ⟨R⟩list_set_rel"
unfolding list_set_rel_def
apply (intro fun_relI)
apply (elim relcompE)
apply (clarsimp simp: br_def)
apply (rule relcompI)
apply (rule param_rev[param_fo], assumption)
apply auto
done

end
```