# Theory Prefix_Tree_Refined

section ‹Refined Code Generation for Prefix Trees›

text ‹This theory provides alternative code equations for selected functions on prefix trees.
Currently only Mapping via RBT is supported.›

theory Prefix_Tree_Refined
imports Prefix_Tree Containers.Containers
begin

declare [[code drop: Prefix_Tree.combine]]

lemma combine_refined[code] :
fixes m1 :: "('a :: ccompare, 'a prefix_tree) mapping_rbt"
shows "Prefix_Tree.combine (MPT (RBT_Mapping m1)) (MPT (RBT_Mapping m2))
= (case ID CCOMPARE('a) of
None  Code.abort (STR ''combine_MPT_RBT_Mapping: ccompare = None'') (λ_. Prefix_Tree.combine (MPT (RBT_Mapping m1)) (MPT (RBT_Mapping m2)))
| Some _  MPT (RBT_Mapping (RBT_Mapping2.join (λ a t1 t2 . Prefix_Tree.combine t1 t2)  m1 m2)))"
(is "?PT1 = ?PT2")
proof (cases "ID CCOMPARE('a)")
case None
then show ?thesis by simp
next
case (Some a)
then have *: "?PT2 = MPT (RBT_Mapping (RBT_Mapping2.join (λ a t1 t2 . Prefix_Tree.combine t1 t2)  m1 m2))"
by auto

have "ID CCOMPARE('a)  None"
using Some by auto

have
proof
fix x

show
(is "?M1 = ?M2")
proof (cases "RBT_Mapping2.lookup m1 x")
case None
show ?thesis proof (cases "RBT_Mapping2.lookup m2 x")
case None

have "?M1 = None"
using  None
by (metis combine_options_simps(1) lookup_Mapping_code(2) lookup_combine)
moreover have "?M2 = None"
using  None
ultimately show ?thesis
by simp
next
case (Some a)
have "?M1 = Some a"
using  Some
by (metis combine_options_simps(1) lookup_Mapping_code(2) lookup_combine)
moreover have "?M2 = Some a"
using  Some
ultimately show ?thesis
by simp
qed
next
case (Some a)
show ?thesis proof (cases "RBT_Mapping2.lookup m2 x")
case None

have "?M1 = Some a"
using None Some
by (metis combine_options_simps(2) lookup_Mapping_code(2) lookup_combine)
moreover have "?M2 = Some a"
using None Some
ultimately show ?thesis
by simp
next
case (Some b)

have "?M1 = Some (Prefix_Tree.combine a b)"
using RBT_Mapping2.lookup m1 x = Some a Some
by (metis combine_options_simps(3) lookup_Mapping_code(2) lookup_combine)
moreover have "?M2 = Some (Prefix_Tree.combine a b)"
using RBT_Mapping2.lookup m1 x = Some a Some
ultimately show ?thesis
by simp
qed
qed
qed
then have "(Mapping.combine Prefix_Tree.combine (RBT_Mapping m1) (RBT_Mapping m2)) = (RBT_Mapping (RBT_Mapping2.join (λ a b c . Prefix_Tree.combine b c) m1 m2))"
by (metis Mapping.lookup.rep_eq rep_inverse)
then show ?thesis
unfolding * unfolding combine_MPT by simp
qed

declare [[code drop: Prefix_Tree.is_leaf]]

lemma is_leaf_refined[code] :
fixes m :: "('a :: ccompare, 'a prefix_tree) mapping_rbt"
shows "Prefix_Tree.is_leaf (MPT (RBT_Mapping m))
= (case ID CCOMPARE('a) of
None  Code.abort (STR ''is_leaf_MPT_RBT_Mapping: ccompare = None'') (λ_. Prefix_Tree.is_leaf (MPT (RBT_Mapping m)))
| Some _  RBT_Mapping2.is_empty m)"
(is "?PT1 = ?PT2")
proof (cases "ID CCOMPARE('a)")
case None
then show ?thesis by simp
next
case (Some a)
then have *: "?PT2 = RBT_Mapping2.is_empty m"
by auto
show ?thesis
unfolding *
by (metis (no_types, opaque_lifting) MPT_def Mapping.is_empty_empty RBT_Mapping2.is_empty_empty Some is_leaf.elims(2) is_leaf_MPT lookup_Mapping_code(2) lookup_empty_empty mapping_empty_code(4) mapping_empty_def option.distinct(1) prefix_tree.inject)
qed

end