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 
          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