# Theory Util_Refined

```section ‹Refinements for Utilities ›

text ‹Introduces program refinement for @{text "Util.thy"}.›

theory Util_Refined
imports Util Containers.Containers
begin

subsection ‹New Code Equations for @{text "set_as_map"}›

declare [[code drop: set_as_map]]

lemma set_as_map_refined[code] :
fixes t :: "('a :: ccompare × 'c :: ccompare) set_rbt"
and   xs:: "('b :: ceq × 'd :: ceq) set_dlist"
shows "set_as_map (RBT_set t) = (case ID CCOMPARE(('a × 'c)) of
Some _ ⇒ Mapping.lookup (RBT_Set2.fold (λ (x,z) m . case Mapping.lookup m (x) of
None ⇒ Mapping.update (x) {z} m |
Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)
t
Mapping.empty) |
None   ⇒ Code.abort (STR ''set_as_map RBT_set: ccompare = None'')
(λ_. set_as_map (RBT_set t)))"
(is "?C1")
and   "set_as_map (DList_set xs) = (case ID CEQ(('b × 'd)) of
Some _ ⇒ Mapping.lookup (DList_Set.fold (λ (x,z) m . case Mapping.lookup m (x) of
None ⇒ Mapping.update (x) {z} m |
Some zs ⇒ Mapping.update (x) (Set.insert z zs) m)
xs
Mapping.empty) |
None   ⇒ Code.abort (STR ''set_as_map RBT_set: ccompare = None'')
(λ_. set_as_map (DList_set xs)))"
(is "?C2")
proof -
show ?C1
proof (cases "ID CCOMPARE(('a × 'c))")
case None
then show ?thesis by auto
next
case (Some a)

let ?f' = "(λ t' . (RBT_Set2.fold (λ (x,z) m . case Mapping.lookup m x of
None ⇒ Mapping.update x {z} m |
Some zs ⇒ Mapping.update x (Set.insert z zs) m)
t'
Mapping.empty))"

let ?f = "λ xs . (fold (λ (x,z) m . case Mapping.lookup m x of
None ⇒ Mapping.update x {z} m |
Some zs ⇒ Mapping.update x (Set.insert z zs) m)
xs Mapping.empty)"
have "⋀ xs :: ('a × 'c) list . Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
proof -
fix xs :: "('a × 'c) list"
show "Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
proof (induction xs rule: rev_induct)
case Nil
then show ?case
next
case (snoc xz xs)
then obtain x z where "xz = (x,z)"
by (metis (mono_tags, opaque_lifting) surj_pair)

have *: "(?f (xs@[(x,z)])) = (case Mapping.lookup (?f xs) x of
None ⇒ Mapping.update x {z} (?f xs) |
Some zs ⇒ Mapping.update x (Set.insert z zs) (?f xs))"
by auto

then show ?case proof (cases "Mapping.lookup (?f xs) x")
case None
then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x {z} (?f xs))" using * by auto

have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
by (metis lookup_update')

have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some {z} else Mapping.lookup (?f xs) x')"
unfolding **
unfolding scheme by force

have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = None"
using None snoc by auto
then have "¬(∃ z . (x,z) ∈ set xs)"
by (metis (mono_tags, lifting) option.distinct(1))
then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" and "{z' . (x,z') ∈ set (xs@[(x,z)])} = {z}"
by fastforce+
then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
= (λ x' . if x' = x then Some {z} else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
by force

show ?thesis using m1 m2 snoc
using ‹xz = (x, z)› by presburger
next
case (Some zs)
then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x (Set.insert z zs) (?f xs))" using * by auto
have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
by (metis lookup_update')

have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some (Set.insert z zs) else Mapping.lookup (?f xs) x')"
unfolding **
unfolding scheme by force

have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs"
using Some snoc by auto
then have "(∃ z' . (x,z') ∈ set xs)"
unfolding case_prod_conv using  option.distinct(2) by metis
then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" by fastforce

have "{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs"
proof -
have "Some {z . (x,z) ∈ set xs} = Some zs"
using ‹(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs›
unfolding case_prod_conv using  option.distinct(2) by metis
then have "{z . (x,z) ∈ set xs} = zs" by auto
then show ?thesis by auto
qed

have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a"
proof -
fix a show "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a"
using ‹{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs› ‹(∃ z' . (x,z') ∈ set (xs@[(x,z)]))›
by (cases "a = x"; auto)
qed

then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
by auto

show ?thesis using m1 m2 snoc
using ‹xz = (x, z)› by presburger
qed
qed
qed
then have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ set (RBT_Set2.keys t)) then Some {z . (x,z) ∈ set (RBT_Set2.keys t)} else None)"
unfolding fold_conv_fold_keys by metis
moreover have "set (RBT_Set2.keys t) = (RBT_set t)"
using Some by (simp add: RBT_set_conv_keys)
ultimately have "Mapping.lookup (?f' t) = (λ x . if (∃ z . (x,z) ∈ (RBT_set t)) then Some {z . (x,z) ∈ (RBT_set t)} else None)"
by force

then show ?thesis
using Some unfolding set_as_map_def by simp
qed

show ?C2
proof (cases "ID CEQ(('b × 'd))")
case None
then show ?thesis by auto
next
case (Some a)

let ?f' = "(λ t' . (DList_Set.fold (λ (x,z) m . case Mapping.lookup m x of
None ⇒ Mapping.update x {z} m |
Some zs ⇒ Mapping.update x (Set.insert z zs) m)
t'
Mapping.empty))"

let ?f = "λ xs . (fold (λ (x,z) m . case Mapping.lookup m x of
None ⇒ Mapping.update x {z} m |
Some zs ⇒ Mapping.update x (Set.insert z zs) m)
xs Mapping.empty)"
have *: "⋀ xs :: ('b × 'd) list . Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
proof -
fix xs :: "('b × 'd) list"
show "Mapping.lookup (?f xs) = (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None)"
proof (induction xs rule: rev_induct)
case Nil
then show ?case
next
case (snoc xz xs)
then obtain x z where "xz = (x,z)"
by (metis (mono_tags, opaque_lifting) surj_pair)

have *: "(?f (xs@[(x,z)])) = (case Mapping.lookup (?f xs) x of
None ⇒ Mapping.update x {z} (?f xs) |
Some zs ⇒ Mapping.update x (Set.insert z zs) (?f xs))"
by auto

then show ?case proof (cases "Mapping.lookup (?f xs) x")
case None
then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x {z} (?f xs))" using * by auto

have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
by (metis lookup_update')

have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some {z} else Mapping.lookup (?f xs) x')"
unfolding **
unfolding scheme by force

have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = None"
using None snoc by auto
then have "¬(∃ z . (x,z) ∈ set xs)"
by (metis (mono_tags, lifting) option.distinct(1))
then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" and "{z' . (x,z') ∈ set (xs@[(x,z)])} = {z}"
by fastforce+
then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
= (λ x' . if x' = x then Some {z} else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
by force

show ?thesis using m1 m2 snoc
using ‹xz = (x, z)› by presburger
next
case (Some zs)
then have **: "Mapping.lookup (?f (xs@[(x,z)])) = Mapping.lookup (Mapping.update x (Set.insert z zs) (?f xs))" using * by auto
have scheme: "⋀ m k v . Mapping.lookup (Mapping.update k v m) = (λk' . if k' = k then Some v else Mapping.lookup m k')"
by (metis lookup_update')

have m1: "Mapping.lookup (?f (xs@[(x,z)])) = (λ x' . if x' = x then Some (Set.insert z zs) else Mapping.lookup (?f xs) x')"
unfolding **
unfolding scheme by force

have "(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs"
using Some snoc by auto
then have "(∃ z' . (x,z') ∈ set xs)"
unfolding case_prod_conv using  option.distinct(2) by metis
then have "(∃ z' . (x,z') ∈ set (xs@[(x,z)]))" by fastforce

have "{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs"
proof -
have "Some {z . (x,z) ∈ set xs} = Some zs"
using ‹(λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x = Some zs›
unfolding case_prod_conv using  option.distinct(2) by metis
then have "{z . (x,z) ∈ set xs} = zs" by auto
then show ?thesis by auto
qed

have "⋀ a  . (λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a"
proof -
fix a show "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None) a
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x') a"
using ‹{z' . (x,z') ∈ set (xs@[(x,z)])} = Set.insert z zs› ‹(∃ z' . (x,z') ∈ set (xs@[(x,z)]))›
by (cases "a = x"; auto)
qed

then have m2: "(λ x' . if (∃ z' . (x',z') ∈ set (xs@[(x,z)])) then Some {z' . (x',z') ∈ set (xs@[(x,z)])} else None)
= (λ x' . if x' = x then Some (Set.insert z zs) else (λ x . if (∃ z . (x,z) ∈ set xs) then Some {z . (x,z) ∈ set xs} else None) x')"
by auto

show ?thesis using m1 m2 snoc
using ‹xz = (x, z)› by presburger
qed
qed
qed

have "ID CEQ('b × 'd) ≠ None"
using Some by auto
then have **: "⋀ x . x ∈ set (list_of_dlist xs) = (x ∈ (DList_set xs))"
using DList_Set.member.rep_eq[of xs]
using Set_member_code(2) ceq_class.ID_ceq in_set_member by fastforce

have "Mapping.lookup (?f' xs) = (λ x . if (∃ z . (x,z) ∈ (DList_set xs)) then Some {z . (x,z) ∈ (DList_set xs)} else None)"
using *[of "(list_of_dlist xs)"]
unfolding DList_Set.fold.rep_eq ** by assumption
then show ?thesis unfolding set_as_map_def using Some by simp
qed
qed

end```