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 by (simp add: Mapping.empty.abs_eq Mapping.lookup.abs_eq) 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 by (simp add: Mapping.empty.abs_eq Mapping.lookup.abs_eq) 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